SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>Propositional formula</title>

</head>

<span id="openzim-page-title" class="mw-page-title-main"><span class="mw-page-title-main">Propositional formula</span></span>

</h1>

</header>

<p>In <a href="Propositional_logic" title="Propositional logic">propositional logic</a>, a <b>propositional formula</b> is a type of syntactic <a href="Formula_(mathematical_logic)" class="mw-redirect" title="Formula (mathematical logic)">formula</a> which is <a href="Well_formed_formula" class="mw-redirect" title="Well formed formula">well formed</a>. If the values of all variables in a propositional formula are given, it determines a unique <a href="Truth_value" title="Truth value">truth value</a>. A propositional formula may also be called a <b>propositional expression</b>, a <b>sentence</b>,<sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> or a <b>sentential formula</b>.

</p><p>A propositional formula is constructed from simple <a href="Proposition_(logic)" class="mw-redirect" title="Proposition (logic)">propositions</a>, such as "five is greater than three" or <a href="Propositional_variable" title="Propositional variable">propositional variables</a> such as <i>p</i> and <i>q</i>, using connectives or <a href="Logical_operator" class="mw-redirect" title="Logical operator">logical operators</a> such as NOT, AND, OR, or IMPLIES; for example:

</p>

<dl><dd>(<i>p</i> AND NOT <i>q</i>) IMPLIES (<i>p</i> OR <i>q</i>).</dd></dl>

<p>In <a href="Mathematics" title="Mathematics">mathematics</a>, a propositional formula is often more briefly referred to as a "<b>proposition</b>", but, more precisely, a propositional formula is not a proposition but a <a href="Formal_expression" class="mw-redirect" title="Formal expression">formal expression</a> that <i>denotes</i> a <a href="Proposition_(mathematics)" class="mw-redirect" title="Proposition (mathematics)">proposition</a>, a <a href="Formal_object" class="mw-redirect" title="Formal object">formal object</a> under discussion, just like an expression such as "<span class="nowrap"><i>x</i> + <i>y</i></span>" is not a value, but denotes a value. In some contexts, maintaining the distinction may be of importance.

</p>

<div class="mw-heading mw-heading2"><h2 id="Propositions">Propositions</h2></div>

<p>For the purposes of the propositional calculus, <b>propositions</b> (utterances, sentences, assertions) are considered to be either simple or compound.<sup id="cite_ref-2" class="reference"><a href="#cite_note-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup> Compound propositions are considered to be linked by sentential connectives, some of the most common of which are "AND", "OR", "IF ... THEN ...", "NEITHER ... NOR ...", "... IS EQUIVALENT TO ..." . The linking semicolon ";", and connective "BUT" are considered to be expressions of "AND". A sequence of discrete sentences are considered to be linked by "AND"s, and formal analysis applies a <a href="Recursion" title="Recursion">recursive</a> "parenthesis rule" with respect to sequences of simple propositions (see more <a href="#Well-formed_formulas_(wffs)">below</a> about well-formed formulas).

</p>

<dl><dd>For example: The assertion: "This cow is blue. That horse is orange but this horse here is purple." is actually a compound proposition linked by "AND"s: ( ("This cow is blue" AND "that horse is orange") AND "this horse here is purple" ) .</dd></dl>

<p>Simple propositions are declarative in nature, that is, they make assertions about the condition or nature of a <i>particular</i> object of sensation e.g. "This cow is blue", "There's a coyote!" ("That coyote IS <i>there</i>, behind the rocks.").<sup id="cite_ref-3" class="reference"><a href="#cite_note-3"><span class="cite-bracket">[</span>3<span class="cite-bracket">]</span></a></sup> Thus the simple "primitive" <a href="Logical_assertion" class="mw-redirect" title="Logical assertion">assertions</a> must be about specific objects or specific states of mind. Each must have at least a subject (an immediate object of thought or observation), a verb (in the active voice and present tense preferred), and perhaps an adjective or adverb. "Dog!" probably implies "I see a dog" but should be rejected as too ambiguous.

</p>

<dl><dd>Example: "That purple dog is running", "This cow is blue", "Switch M31 is closed", "This cap is off", "Tomorrow is Friday".</dd></dl>

<p>For the purposes of the propositional calculus a compound proposition can usually be reworded into a series of simple sentences, although the result will probably sound stilted.

</p>

<div class="mw-heading mw-heading3"><h3 id="Relationship_between_propositional_and_predicate_formulas">Relationship between propositional and predicate formulas</h3></div>

<p>The <a href="Predicate_calculus" class="mw-redirect" title="Predicate calculus">predicate calculus</a> goes a step further than the propositional calculus to an "analysis of the <i>inner structure</i> of propositions"<sup id="cite_ref-4" class="reference"><a href="#cite_note-4"><span class="cite-bracket">[</span>4<span class="cite-bracket">]</span></a></sup> It breaks a simple sentence down into two parts (i) its subject (the object (<a href="Singular_term" title="Singular term">singular</a> or plural) of discourse) and (ii) a <a href="Predicate_(grammar)" title="Predicate (grammar)">predicate</a> (a verb or possibly verb-clause that asserts a quality or attribute of the object(s)). The predicate calculus then generalizes the "subject|predicate" form (where | symbolizes <a href="Concatenation" title="Concatenation">concatenation</a> (stringing together) of symbols) into a form with the following blank-subject structure " ___|predicate", and the predicate in turn generalized to all things with that property.

</p>

<dl><dd>Example: "This blue pig has wings" becomes two sentences in the <i>propositional calculus</i>: "This pig has wings" AND "This pig is blue", whose internal structure is not considered. In contrast, in the predicate calculus, the first sentence breaks into "this pig" as the subject, and "has wings" as the predicate. Thus it asserts that object "this pig" is a member of the class (set, collection) of "winged things". The second sentence asserts that object "this pig" has an attribute "blue" and thus is a member of the class of "blue things". One might choose to write the two sentences connected with AND as:

<p>The generalization of "this pig" to a (potential) member of two classes "winged things" and "blue things" means that it has a truth-relationship with both of these classes. In other words, given a <a href="Domain_of_discourse" title="Domain of discourse">domain of discourse</a> "winged things", p is either found to be a member of this domain or not. Thus there is a relationship W (wingedness) between p (pig) and { T, F }, W(p) evaluates to { T, F } where { T, F } is the set of the <a href="Boolean_data_type" title="Boolean data type">Boolean values</a> "true" and "false". Likewise for B (blueness) and p (pig) and { T, F }: B(p) evaluates to { T, F }. So one now can analyze the connected assertions "B(p) AND W(p)" for its overall truth-value, i.e.:

</p>

<dl><dd>( B(p) AND W(p) ) evaluates to { T, F }</dd></dl>

<p>In particular, simple sentences that employ notions of "all", "some", "a few", "one of", etc. called <a href="Logical_quantifier" class="mw-redirect" title="Logical quantifier">logical quantifiers</a> are treated by the predicate calculus. Along with the new function symbolism "F(x)" two new symbols are introduced: ∀ (For all), and ∃ (There exists ..., At least one of ... exists, etc.). The predicate calculus, but not the propositional calculus, can establish the formal validity of the following statement:

</p>

<dl><dd>"All blue pigs have wings but some pigs have no wings, hence some pigs are not blue".</dd></dl>

<div class="mw-heading mw-heading3"><h3 id="Identity">Identity</h3></div>

<p>Tarski asserts that the notion of IDENTITY (as distinguished from LOGICAL EQUIVALENCE) lies outside the propositional calculus; however, he notes that if a logic is to be of use for mathematics and the sciences it must contain a "theory" of IDENTITY.<sup id="cite_ref-5" class="reference"><a href="#cite_note-5"><span class="cite-bracket">[</span>5<span class="cite-bracket">]</span></a></sup> Some authors refer to "predicate logic with identity" to emphasize this extension. See more about this below.

</p>

<div class="mw-heading mw-heading2"><h2 id="An_algebra_of_propositions,_the_propositional_calculus">An algebra of propositions, the propositional calculus</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .ambox{border:1px solid #a2a9b1;border-left:10px solid #36c;background-color:#fbfbfb;box-sizing:border-box}.mw-parser-output .ambox+link+.ambox,.mw-parser-output .ambox+link+style+.ambox,.mw-parser-output .ambox+link+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+style+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+link+.ambox{margin-top:-1px}html body.mediawiki .mw-parser-output .ambox.mbox-small-left{margin:4px 1em 4px 0;overflow:hidden;width:238px;border-collapse:collapse;font-size:88%;line-height:1.25em}.mw-parser-output .ambox-speedy{border-left:10px solid #b32424;background-color:#fee7e6}.mw-parser-output .ambox-delete{border-left:10px solid #b32424}.mw-parser-output .ambox-content{border-left:10px solid #f28500}.mw-parser-output .ambox-style{border-left:10px solid #fc3}.mw-parser-output .ambox-move{border-left:10px solid #9932cc}.mw-parser-output .ambox-protection{border-left:10px solid #a2a9b1}.mw-parser-output .ambox .mbox-text{border:none;padding:0.25em 0.5em;width:100%}.mw-parser-output .ambox .mbox-image{border:none;padding:2px 0 2px 0.5em;text-align:center}.mw-parser-output .ambox .mbox-imageright{border:none;padding:2px 0.5em 2px 0;text-align:center}.mw-parser-output .ambox .mbox-empty-cell{border:none;padding:0;width:1px}.mw-parser-output .ambox .mbox-image-div{width:52px}@media(min-width:720px){.mw-parser-output .ambox{margin:0 10%}}@media print{body.ns-0 .mw-parser-output .ambox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style>

<p>An algebra (and there are many different ones), loosely defined, is a method by which a collection of symbols called variables together with some other symbols such as parentheses (, ) and some sub-set of symbols such as *, +, ~, &, ∨, =, ≡, ∧, ￢ are manipulated within a system of rules. These symbols, and well-formed strings of them, are said to represent objects, but in a specific algebraic system these objects do not have meanings. Thus work inside the algebra becomes an exercise in obeying certain laws (rules) of the algebra's <a href="Syntax" title="Syntax">syntax</a> (symbol-formation) rather than in <a href="Semantics" title="Semantics">semantics</a> (meaning) of the symbols. The meanings are to be found outside the algebra.

</p><p>For a well-formed sequence of symbols in the algebra —a formula— to have some usefulness outside the algebra the symbols are assigned meanings and eventually the variables are assigned values; then by a series of rules the formula is evaluated.

</p><p>When the values are restricted to just two and applied to the notion of simple sentences (e.g. spoken utterances or written assertions) linked by propositional connectives this whole algebraic system of symbols and rules and evaluation-methods is usually called the <a href="Propositional_calculus" class="mw-redirect" title="Propositional calculus">propositional calculus</a> or the sentential calculus.

</p><p>While some of the familiar rules of arithmetic algebra continue to hold in the algebra of propositions (e.g. the commutative and associative laws for AND and OR), some do not (e.g. the <a href="Distributive_law" class="mw-redirect" title="Distributive law">distributive laws</a> for AND, OR and NOT).

</p>

<div class="mw-heading mw-heading3"><h3 id="Usefulness_of_propositional_formulas">Usefulness of propositional formulas</h3></div>

<p>Analysis: In <a href="Deductive_reasoning" title="Deductive reasoning">deductive reasoning</a>, philosophers, rhetoricians and mathematicians reduce arguments to formulas and then study them (usually with <a href="Truth_table" title="Truth table">truth tables</a>) for correctness (soundness). For example: Is the following argument sound?

</p>

<dl><dd>"Given that consciousness is sufficient for an <a href="Artificial_intelligence" title="Artificial intelligence">artificial intelligence</a> and only conscious entities can pass the <a href="Turing_test" title="Turing test">Turing test</a>, before we can conclude that a robot is an artificial intelligence the robot must pass the Turing test."</dd></dl>

<p>Engineers analyze the <a href="Logic_circuits" class="mw-redirect" title="Logic circuits">logic circuits</a> they have designed using synthesis techniques and then apply various reduction and minimization techniques to simplify their designs.

</p><p>Synthesis: Engineers in particular synthesize propositional formulas (that eventually end up as circuits of symbols) from <a href="Truth_table" title="Truth table">truth tables</a>. For example, one might write down a truth table for how <a href="Binary_addition" class="mw-redirect" title="Binary addition">binary addition</a> should behave given the addition of variables "b" and "a" and "carry_in" "ci", and the results "carry_out" "co" and "sum" Σ:

</p>

<ul><li>Example: in row 5, ( (b+a) + ci ) = ( (1+0) + 1 ) = the number "2". written as a binary number this is 10<sub>2</sub>, where "co"=1 and Σ=0 as shown in the right-most columns.</li></ul>

<th>row

</th>

<th>Σ

</th></tr>

<tr>

<th>0

</th>

<td>0

</td></tr>

<tr>

<th>1

</th>

<td>1

</td></tr>

<tr>

<th>2

</th>

<td>1

</td></tr>

<tr>

<th>3

</th>

<td>0

</td></tr>

<tr>

<th>4

</th>

<td>1

</td></tr>

<tr>

<th>5

</th>

<td>0

</td></tr>

<tr>

<th>6

</th>

<td>0

</td></tr>

<tr>

<th>7

</th>

<td>1

</td></tr></tbody></table>

<div class="mw-heading mw-heading3"><h3 id="Propositional_variables">Propositional variables</h3></div>

<p>The simplest type of propositional formula is a <b><a href="Propositional_variable" title="Propositional variable">propositional variable</a></b>. Propositions that are simple (<a href="Atomic_formula" title="Atomic formula">atomic</a>), symbolic expressions are often denoted by variables named <i>p</i>, <i>q</i>, or <i>P</i>, <i>Q</i>, etc. A propositional variable is intended to represent an atomic proposition (assertion), such as "It is Saturday" = <i>p</i> (here the symbol = means " ... is assigned the variable named ...") or "I only go to the movies on Monday" = <i>q</i>.

</p>

<div class="mw-heading mw-heading3"><h3 id="Truth-value_assignments,_formula_evaluations">Truth-value assignments, formula evaluations</h3></div>

<p>Evaluation of a propositional formula begins with assignment of a truth value to each variable. Because each variable represents a simple sentence, the truth values are being applied to the "truth" or "falsity" of these simple sentences.

</p><p><b>Truth values in rhetoric, philosophy and mathematics</b>

</p><p>The truth values are only two: { TRUTH "T", FALSITY "F" }. An <a href="Empiricist" class="mw-redirect" title="Empiricist">empiricist</a> puts all propositions into two broad classes: <i>analytic</i>—true no matter what (e.g. <a href="Tautology_(logic)" title="Tautology (logic)">tautology</a>), and <i>synthetic</i>—derived from experience and thereby susceptible to confirmation by third parties (the <a href="Verification_theory" class="mw-redirect" title="Verification theory">verification theory</a> of meaning).<sup id="cite_ref-6" class="reference"><a href="#cite_note-6"><span class="cite-bracket">[</span>6<span class="cite-bracket">]</span></a></sup> Empiricists hold that, in general, to arrive at the truth-value of a <a href="Synthetic_proposition" class="mw-redirect" title="Synthetic proposition">synthetic proposition</a>, meanings (pattern-matching templates) must first be applied to the words, and then these meaning-templates must be matched against whatever it is that is being asserted. For example, my utterance "That cow is <i><span style="color:blue">blue</span></i>!" Is this statement a TRUTH? Truly I said it. And maybe I <i>am</i> seeing a blue cow—unless I am lying my statement is a TRUTH relative to the object of my (perhaps flawed) perception. But is the blue cow "really there"? What do you see when you look out the same window? In order to proceed with a verification, you will need a prior notion (a template) of both "cow" and "<span style="color:blue">blue</span>", and an ability to match the templates against the object of sensation (if indeed there is one).

</p><p><b>Truth values in engineering</b>

</p><p>Engineers try to avoid notions of truth and falsity that bedevil philosophers, but in the final analysis engineers must trust their measuring instruments. In their quest for <a href="Robust_statistics" title="Robust statistics">robustness</a>, engineers prefer to pull known objects from a small library—objects that have well-defined, predictable behaviors even in large combinations, (hence their name for the propositional calculus: "combinatorial logic"). The fewest behaviors of a single object are two (e.g. { OFF, ON }, { open, shut }, { UP, DOWN } etc.), and these are put in correspondence with { 0, 1 }. Such elements are called <a href="Digital_data" title="Digital data">digital</a>; those with a continuous range of behaviors are called <a href="Analog_signal" title="Analog signal">analog</a>. Whenever decisions must be made in an analog system, quite often an engineer will convert an analog behavior (the door is 45.32146% UP) to digital (e.g. DOWN=0 ) by use of a <a href="Comparator" title="Comparator">comparator</a>.<sup id="cite_ref-7" class="reference"><a href="#cite_note-7"><span class="cite-bracket">[</span>7<span class="cite-bracket">]</span></a></sup>

</p><p>Thus an assignment of meaning of the variables and the two value-symbols { 0, 1 } comes from "outside" the formula that represents the behavior of the (usually) compound object. An example is a garage door with two "limit switches", one for UP labelled SW_U and one for DOWN labelled SW_D, and whatever else is in the door's circuitry. Inspection of the circuit (either the diagram or the actual objects themselves—door, switches, wires, circuit board, etc.) might reveal that, on the circuit board "node 22" goes to +0 volts when the contacts of switch "SW_D" are mechanically in contact ("closed") and the door is in the "down" position (95% down), and "node 29" goes to +0 volts when the door is 95% UP and the contacts of switch SW_U are in mechanical contact ("closed").<sup id="cite_ref-8" class="reference"><a href="#cite_note-8"><span class="cite-bracket">[</span>8<span class="cite-bracket">]</span></a></sup> The engineer must define the meanings of these voltages and all possible combinations (all 4 of them), including the "bad" ones (e.g. both nodes 22 and 29 at 0 volts, meaning that the door is open and closed at the same time). The circuit mindlessly responds to whatever voltages it experiences without any awareness of TRUTH or FALSEHOOD, RIGHT or WRONG, SAFE or DANGEROUS.

</p>

<div class="mw-heading mw-heading2"><h2 id="Propositional_connectives">Propositional connectives</h2></div>

<p>Arbitrary propositional formulas are built from propositional variables and other propositional formulas using <a href="Logical_connective" title="Logical connective">propositional connectives</a>. Examples of connectives include:

</p>

<ul><li>The unary negation connective. If <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \alpha }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \alpha }</annotation>

</semantics>

</math></span><img src="./b79333175c8b3f0840bfb4ec41b8072c83ea88d3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.488ex; height:1.676ex;" alt="{\displaystyle \alpha }" loading="lazy"></span> is a formula, then <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot \alpha }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \lnot \alpha }</annotation>

</semantics>

</math></span><img src="./e9a1860c0e332d32f8e76cbfb6eb08c2a3259ca8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:3.038ex; height:1.676ex;" alt="{\displaystyle \lnot \alpha }" loading="lazy"></span> is a formula.</li>

<li>The classical binary connectives <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \land ,\lor ,\to ,\leftrightarrow }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \land ,\lor ,\to ,\leftrightarrow }</annotation>

</semantics>

</math></span><img src="./80a90c332534b2007a1252f56b93a9f7cb170156.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:10.85ex; height:2.343ex;" alt="{\displaystyle \land ,\lor ,\to ,\leftrightarrow }" loading="lazy"></span>. Thus, for example, if <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \alpha }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \alpha }</annotation>

</semantics>

</math></span><img src="./b79333175c8b3f0840bfb4ec41b8072c83ea88d3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.488ex; height:1.676ex;" alt="{\displaystyle \alpha }" loading="lazy"></span> and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \beta }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \beta }</annotation>

</semantics>

</math></span><img src="./7ed48a5e36207156fb792fa79d29925d2f7901e8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.332ex; height:2.509ex;" alt="{\displaystyle \beta }" loading="lazy"></span> are formulas, so is <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (\alpha \to \beta )}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (\alpha \to \beta )}</annotation>

</semantics>

</math></span><img src="./e999b99300443b6865cfb51644e0e1ed723e0601.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:8.243ex; height:2.843ex;" alt="{\displaystyle (\alpha \to \beta )}" loading="lazy"></span>.</li>

<li>Other binary connectives, such as NAND, NOR, and XOR</li>

<li>The ternary connective IF ... THEN ... ELSE ...</li>

<li>Constant 0-ary connectives ⊤ and ⊥ (alternately, constants { T, F }, { 1, 0 } etc. )</li>

<li>The "theory-extension" connective EQUALS (alternately, IDENTITY, or the sign " = " as distinguished from the "logical connective" <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \leftrightarrow }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \leftrightarrow }</annotation>

</semantics>

</math></span><img src="./046b918c43e05caf6624fe9b676c69ec9cd6b892.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.324ex; height:1.843ex;" alt="{\displaystyle \leftrightarrow }" loading="lazy"></span>)</li></ul>

<div class="mw-heading mw-heading3"><h3 id="Connectives_of_rhetoric,_philosophy_and_mathematics">Connectives of rhetoric, philosophy and mathematics</h3></div>

<p>The following are the connectives common to rhetoric, philosophy and mathematics together with their <a href="Truth_table" title="Truth table">truth tables</a>. The symbols used will vary from author to author and between fields of endeavor. In general the abbreviations "T" and "F" stand for the evaluations TRUTH and FALSITY applied to the variables in the propositional formula (e.g. the assertion: "That cow is blue" will have the truth-value "T" for Truth or "F" for Falsity, as the case may be.).

</p><p>The connectives go by a number of different word-usages, e.g. "a IMPLIES b" is also said "IF a THEN b". Some of these are shown in the table.

</p>

</td>

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#E5E0EC" width="114.75">b only if a

</td>

</td>

</td>

</td>

</td>

</td></tr>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#E5E0EC">b IS SUFFICIENT FOR a

</td>

<td style="background-color:#F2F2F2">b PRECISELY WHEN a

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td></tr>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#E5E0EC">a IS NECESSARY FOR b

</td>

<td style="background-color:#F2F2F2">b IF AND ONLY IF a; b IFF a

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td></tr>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#FDE9D9">inclusive OR

</td>

<td style="background-color:#E5E0EC">IF b THEN a

</td>

<td style="background-color:#F2F2F2">b IS NECESSARY AND SUFFICIENT FOR a

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td></tr>

</td>

<td>

</td>

<td style="background-color:#EAF1DD">negation

</td>

<td style="background-color:#EAF1DD">negation

</td>

<td style="background-color:#DBE5F1">conjunction

</td>

<td style="background-color:#FDE9D9">disjunction

</td>

<td style="background-color:#E5E0EC">implication

</td>

<td style="background-color:#F2F2F2">biconditional

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td></tr>

<th height="12" colspan="2">variables

</th>

<td style="background-color:#EAF1DD">NOT b

</td>

<td style="background-color:#EAF1DD">NOT a

</td>

<td style="background-color:#DBE5F1">b AND a

</td>

<td style="background-color:#FDE9D9">b OR a

</td>

<td style="background-color:#E5E0EC">b IMPLIES a

</td>

<td style="background-color:#F2F2F2">b IS <a href="Logical_equivalence" title="Logical equivalence">logically equivalent</a> TO a ***

</td>

<td>f IS A tautology

</td>

<td>NEITHER a NOR b

</td>

<td>b stroke a

</td>

<td>exclusive OR

</td></tr>

<td style="font-weight:bold" height="12">b

</td>

<td style="font-weight:bold">a

</td>

<td style="background-color:#EAF1DD;font-weight:bold">¬(b)

</td>

<td style="background-color:#EAF1DD;font-weight:bold">¬(a)

</td>

<td style="background-color:#DBE5F1;font-weight:bold">(b ∧ a)

</td>

<td style="background-color:#FDE9D9;font-weight:bold">(b ∨ a)

</td>

<td style="background-color:#E5E0EC;font-weight:bold">(b → a)

</td>

<td style="background-color:#F2F2F2;font-weight:bold">(b ↔ a)

</td>

<td>(f = formula)

</td>

<td>(a NOR b)

</td>

<td style="font-weight:bold">(b|a)

</td>

<td style="font-weight:bold">various

</td></tr>

<td height="12">F

</td>

<td>F

</td>

<td style="background-color:#EAF1DD">T

</td>

<td style="background-color:#EAF1DD">T

</td>

<td style="background-color:#DBE5F1">F

</td>

<td style="background-color:#FDE9D9">F

</td>

<td style="background-color:#E5E0EC;font-size:9pt">T

</td>

<td style="background-color:#F2F2F2;font-size:9pt">T

</td>

<td style="font-size:9pt">T

</td>

<td style="font-size:9pt">T

</td>

<td>T

</td>

<td style="font-size:9pt">F

</td></tr>

<td height="12">F

</td>

<td style="font-size:9pt">T

</td>

<td style="background-color:#EAF1DD">T

</td>

<td style="background-color:#EAF1DD;font-size:9pt">F

</td>

<td style="background-color:#DBE5F1">F

</td>

<td style="background-color:#FDE9D9;font-size:9pt">T

</td>

<td style="background-color:#E5E0EC;font-size:9pt">T

</td>

<td style="background-color:#F2F2F2;font-size:9pt">F

</td>

<td style="font-size:9pt">T

</td>

<td style="font-size:9pt">F

</td>

<td>T

</td>

<td style="font-size:9pt">T

</td></tr>

<td style="font-size:9pt" height="12">T

</td>

<td>F

</td>

<td style="background-color:#EAF1DD">F

</td>

<td style="background-color:#EAF1DD">T

</td>

<td style="background-color:#DBE5F1">F

</td>

<td style="background-color:#FDE9D9;font-size:9pt">T

</td>

<td style="background-color:#E5E0EC;font-size:9pt">F

</td>

<td style="background-color:#F2F2F2;font-size:9pt">F

</td>

<td style="font-size:9pt">T

</td>

<td style="font-size:9pt">F

</td>

<td>T

</td>

<td style="font-size:9pt">T

</td></tr>

<td style="font-size:9pt" height="12">T

</td>

<td style="font-size:9pt">T

</td>

<td style="background-color:#EAF1DD">F

</td>

<td style="background-color:#EAF1DD;font-size:9pt">F

</td>

<td style="background-color:#DBE5F1;font-size:9pt">T

</td>

<td style="background-color:#FDE9D9;font-size:9pt">T

</td>

<td style="background-color:#E5E0EC;font-size:9pt">T

</td>

<td style="background-color:#F2F2F2;font-size:9pt">T

</td>

<td style="font-size:9pt">T

</td>

<td style="font-size:9pt">F

</td>

<td style="font-size:9pt">F

</td>

<td style="font-size:9pt">F

</td></tr></tbody></table>

<div class="mw-heading mw-heading3"><h3 id="Engineering_connectives">Engineering connectives</h3></div>

<p>In general, the engineering connectives are just the same as the mathematics connectives excepting they tend to evaluate with "1" = "T" and "0" = "F". This is done for the purposes of analysis/minimization and synthesis of formulas by use of the notion of <i>minterms</i> and <a href="Karnaugh_map" title="Karnaugh map">Karnaugh maps</a> (see below). Engineers also use the words <b>logical product</b> from <a href="Boole" class="mw-redirect" title="Boole">Boole</a>'s notion (a*a = a) and <b>logical sum</b> from <a href="William_Stanley_Jevons" title="William Stanley Jevons">Jevons</a>' notion (a+a = a).<sup id="cite_ref-9" class="reference"><a href="#cite_note-9"><span class="cite-bracket">[</span>9<span class="cite-bracket">]</span></a></sup>

</p>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<th rowspan="2">logical product

</th>

<th rowspan="2">logical sum

</th>

<td>

</td>

<td>

</td>

<th>half-adder<br>(no carry)

</th></tr>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<th>exclusive OR

</th></tr>

<th height="12">row number

</th>

<th colspan="2">variables

</th>

<td style="background-color:#EAF1DD">NOT

</td>

<td style="background-color:#EAF1DD">NOT

</td>

<td style="background-color:#DBE5F1">AND

</td>

<td style="background-color:#FDE9D9">OR

</td>

<td>NAND

</td>

<td>NOR

</td>

<td>XOR

</td></tr>

<tr>

</td>

<td style="font-size:9pt;font-weight:bold">b

</td>

<td style="font-size:9pt;font-weight:bold">a

</td>

<td style="background-color:#EAF1DD;font-size:9pt;font-weight:bold;white-space:nowrap;">~(b)

</td>

<td style="background-color:#EAF1DD;font-size:9pt;font-weight:bold;white-space:nowrap;">~(a)

</td>

<td style="background-color:#DBE5F1;font-size:9pt;font-weight:bold;white-space:nowrap;">(b & a)

</td>

<td style="background-color:#FDE9D9;font-size:9pt;font-weight:bold;white-space:nowrap;">(b ∨ a)

</td>

<td style="font-size:9pt;font-weight:bold;white-space:nowrap;">~(b & a)

</td>

<td style="font-size:9pt;font-weight:bold;white-space:nowrap;">~(b ∨ a)

</td>

<td style="font-size:14pt">⊕

</td></tr>

<tr>

<td style="font-size:9pt" height="12">0

</td>

<td>0

</td>

<td>0

</td>

<td style="background-color:#EAF1DD">1

</td>

<td style="background-color:#EAF1DD">1

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#FDE9D9">0

</td>

<td style="font-size:9pt">1

</td>

<td style="font-size:9pt">1

</td>

<td style="font-size:9pt">0

</td></tr>

<tr>

<td style="font-size:9pt" height="12">1

</td>

<td>0

</td>

<td style="font-size:9pt">1

</td>

<td style="background-color:#EAF1DD">1

</td>

<td style="background-color:#EAF1DD;font-size:9pt">0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#FDE9D9;font-size:9pt">1

</td>

<td style="font-size:9pt">1

</td>

<td style="font-size:9pt">0

</td>

<td style="font-size:9pt">1

</td></tr>

<tr>

<td style="font-size:9pt" height="12">2

</td>

<td style="font-size:9pt">1

</td>

<td>0

</td>

<td style="background-color:#EAF1DD">0

</td>

<td style="background-color:#EAF1DD">1

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#FDE9D9;font-size:9pt">1

</td>

<td style="font-size:9pt">1

</td>

<td style="font-size:9pt">0

</td>

<td style="font-size:9pt">1

</td></tr>

<tr>

<td style="font-size:9pt" height="12">3

</td>

<td style="font-size:9pt">1

</td>

<td style="font-size:9pt">1

</td>

<td style="background-color:#EAF1DD">0

</td>

<td style="background-color:#EAF1DD">0

</td>

<td style="background-color:#DBE5F1;font-size:9pt">1

</td>

<td style="background-color:#FDE9D9;font-size:9pt">1

</td>

<td style="font-size:9pt">0

</td>

<td style="font-size:9pt">0

</td>

<td style="font-size:9pt">0

</td></tr></tbody></table>

<div class="mw-heading mw-heading3"><h3 id="CASE_connective:_IF_..._THEN_..._ELSE_...">CASE connective: IF ... THEN ... ELSE ...</h3></div>

<p>The IF ... THEN ... ELSE ... connective appears as the simplest form of CASE operator of <a href="Recursion_theory" class="mw-redirect" title="Recursion theory">recursion theory</a> and <a href="Computation_theory" class="mw-redirect" title="Computation theory">computation theory</a> and is the connective responsible for conditional goto's (jumps, branches). From this one connective all other connectives can be constructed (see more below). Although " IF c THEN b ELSE a " sounds like an implication it is, in its most reduced form, a switch that makes a decision and offers as outcome only one of two alternatives "a" or "b" (hence the name <a href="Switch_statement" title="Switch statement">switch statement</a> in the <a href="C_(programming_language)" title="C (programming language)">C</a> programming language).<sup id="cite_ref-10" class="reference"><a href="#cite_note-10"><span class="cite-bracket">[</span>10<span class="cite-bracket">]</span></a></sup>

</p><p>The following three propositions are equivalent (as indicated by the logical equivalence sign ≡ ):

</p>

<ol><li>( IF 'counter is zero' THEN 'go to instruction <i>b</i> ' ELSE 'go to instruction <i>a</i> ') ≡</li>

<li>( (c → b) & (~c → a) ) ≡ ( ( IF 'counter is zero' THEN 'go to instruction <i>b</i> ' ) AND ( IF 'It is NOT the case that counter is zero' THEN 'go to instruction <i>a</i> ) " ≡</li>

<li>( (c & b) ∨ (~c & a) ) ≡ " ( 'Counter is zero' AND 'go to instruction <i>b</i> ) OR ( 'It is NOT the case that 'counter is zero' AND 'go to instruction <i>a</i> ) "</li></ol>

<p>Thus IF ... THEN ... ELSE—unlike implication—does not evaluate to an ambiguous "TRUTH" when the first proposition is false i.e. c = F in (c → b). For example, most people would reject the following compound proposition as a nonsensical <i>non sequitur</i> because the second sentence is <i>not connected in meaning</i> to the first.<sup id="cite_ref-11" class="reference"><a href="#cite_note-11"><span class="cite-bracket">[</span>11<span class="cite-bracket">]</span></a></sup>

</p>

<dl><dd>Example: The proposition " IF 'Winston Churchill was Chinese' THEN 'The sun rises in the east' " evaluates as a TRUTH given that 'Winston Churchill was Chinese' is a FALSEHOOD and 'The sun rises in the east' evaluates as a TRUTH.</dd></dl>

<p>In recognition of this problem, the sign → of formal implication in the propositional calculus is called <a href="Material_conditional" title="Material conditional">material implication</a> to distinguish it from the everyday, intuitive implication.<sup id="cite_ref-13" class="reference"><a href="#cite_note-13"><span class="cite-bracket">[</span>a<span class="cite-bracket">]</span></a></sup>

</p><p>The use of the IF ... THEN ... ELSE construction avoids controversy because it offers a completely deterministic choice between two stated alternatives; it offers two "objects" (the two alternatives b and a), and it <i>selects</i> between them exhaustively and unambiguously.<sup id="cite_ref-14" class="reference"><a href="#cite_note-14"><span class="cite-bracket">[</span>13<span class="cite-bracket">]</span></a></sup> In the truth table below, d1 is the formula: ( (IF c THEN b) AND (IF NOT-c THEN a) ). Its fully reduced form d2 is the formula: ( (c AND b) OR (NOT-c AND a). The two formulas are equivalent as shown by the columns "=d1" and "=d2". Electrical engineers call the fully reduced formula the AND-OR-SELECT operator. The CASE (or SWITCH) operator is an extension of the same idea to <i>n</i> possible, but mutually exclusive outcomes. Electrical engineers call the CASE operator a <a href="Multiplexer" title="Multiplexer">multiplexer</a>.

</p>

<table>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#FDE9D9" width="17.25">d1

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#FDE9D9" width="15.75">d2

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td></tr>

<th style="background-color:#F2F2F2" height="12">row

</th>

<th>c

</th>

<th>b

</th>

<th>a

</th>

</td>

<td>(

</td>

<td>(

</td>

<td>c

</td>

<td>→

</td>

<td>b

</td>

<td>)

</td>

<td style="background-color:#FDE9D9">&

</td>

<td>(

</td>

<td style="background-color:#EAF1DD">~

</td>

<td>(

</td>

<td>c

</td>

<td>)

</td>

<td>→

</td>

<td>a

</td>

<td>)

</td>

<td>)

</td>

<td style="background-color:#FDE9D9">=d1

</td>

</td>

<td>(

</td>

<td>(

</td>

<td>c

</td>

<td style="background-color:#DBEEF3">&

</td>

<td>b

</td>

<td>)

</td>

<td style="background-color:#FDE9D9">∨

</td>

<td>(

</td>

<td style="background-color:#EAF1DD">~

</td>

<td>(

</td>

<td>c

</td>

<td>)

</td>

<td style="background-color:#DBE5F1">&

</td>

<td>a

</td>

<td>)

</td>

<td>)

</td>

<td style="background-color:#FDE9D9">=d2

</td></tr>

<td style="background-color:#F2F2F2" height="12">0

</td>

<td>0

</td>

<td>0

</td>

<td style="background-color:#C5D9F1">0

</td>

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td>1

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#B8CCE4">0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#B8CCE4">0

</td>

<td style="background-color:#B8CCE4">0

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#B8CCE4">0

</td>

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td>0

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#B8CCE4">0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#B8CCE4">0

</td>

<td style="background-color:#B8CCE4">0

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#B8CCE4">0

</td></tr>

<td style="background-color:#F2F2F2" height="12">1

</td>

<td>0

</td>

<td>0

</td>

<td style="background-color:#C5D9F1">1

</td>

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td>1

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#B8CCE4">1

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#B8CCE4">1

</td>

<td style="background-color:#B8CCE4">1

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#B8CCE4">1

</td>

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td>0

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#B8CCE4">1

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#B8CCE4">1

</td>

<td style="background-color:#B8CCE4">1

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#B8CCE4">1

</td></tr>

<td style="background-color:#F2F2F2" height="12">2

</td>

<td>0

</td>

<td>1

</td>

<td style="background-color:#C5D9F1">0

</td>

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td>1

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#B8CCE4">0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#B8CCE4">0

</td>

<td style="background-color:#B8CCE4">0

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#B8CCE4">0

</td>

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td>0

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#B8CCE4">0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#B8CCE4">0

</td>

<td style="background-color:#B8CCE4">0

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#B8CCE4">0

</td></tr>

<td style="background-color:#F2F2F2" height="12">3

</td>

<td>0

</td>

<td>1

</td>

<td style="background-color:#C5D9F1">1

</td>

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td>1

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#B8CCE4">1

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#B8CCE4">1

</td>

<td style="background-color:#B8CCE4">1

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#B8CCE4">1

</td>

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td>0

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#B8CCE4">1

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#B8CCE4">1

</td>

<td style="background-color:#B8CCE4">1

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#B8CCE4">1

</td></tr>

<td style="background-color:#F2F2F2" height="12">4

</td>

<td>1

</td>

<td style="background-color:#DBEEF3">0

</td>

<td>0

</td>

</td>

<td>

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBEEF3">0

</td>

<td style="background-color:#DBEEF3">0

</td>

<td>

</td>

<td style="background-color:#DBEEF3">0

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>1

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#DBEEF3">0

</td>

</td>

<td>

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBEEF3">0

</td>

<td style="background-color:#DBEEF3">0

</td>

<td>

</td>

<td style="background-color:#DBEEF3">0

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>0

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#DBEEF3">0

</td></tr>

<td style="background-color:#F2F2F2" height="12">5

</td>

<td>1

</td>

<td style="background-color:#DBEEF3">0

</td>

<td>1

</td>

</td>

<td>

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBEEF3">0

</td>

<td style="background-color:#DBEEF3">0

</td>

<td>

</td>

<td style="background-color:#DBEEF3">0

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>1

</td>

<td>1

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#DBEEF3">0

</td>

</td>

<td>

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBEEF3">0

</td>

<td style="background-color:#DBEEF3">0

</td>

<td>

</td>

<td style="background-color:#DBEEF3">0

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>0

</td>

<td>1

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#DBEEF3">0

</td></tr>

<td style="background-color:#F2F2F2" height="12">6

</td>

<td>1

</td>

<td style="background-color:#DBEEF3">1

</td>

<td>0

</td>

</td>

<td>

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBEEF3">1

</td>

<td style="background-color:#DBEEF3">1

</td>

<td>

</td>

<td style="background-color:#DBEEF3">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>1

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#DBEEF3">1

</td>

</td>

<td>

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBEEF3">1

</td>

<td style="background-color:#DBEEF3">1

</td>

<td>

</td>

<td style="background-color:#DBEEF3">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>0

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#DBEEF3">1

</td></tr>

<td style="background-color:#F2F2F2" height="12">7

</td>

<td>1

</td>

<td style="background-color:#DBEEF3">1

</td>

<td>1

</td>

</td>

<td>

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBEEF3">1

</td>

<td style="background-color:#DBEEF3">1

</td>

<td>

</td>

<td style="background-color:#DBEEF3">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>1

</td>

<td>1

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#DBEEF3">1

</td>

</td>

<td>

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBEEF3">1

</td>

<td style="background-color:#DBEEF3">1

</td>

<td>

</td>

<td style="background-color:#DBEEF3">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>0

</td>

<td>1

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#DBEEF3">1

</td></tr></tbody></table>

<div class="mw-heading mw-heading3"><h3 id="IDENTITY_and_evaluation">IDENTITY and evaluation</h3></div>

<p>The first table of this section stars *** the entry logical equivalence to note the fact that "<a href="Logical_equivalence" title="Logical equivalence">Logical equivalence</a>" is not the same thing as "identity". For example, most would agree that the assertion "That cow is blue" is identical to the assertion "That cow is blue". On the other hand, <i>logical</i> equivalence sometimes appears in speech as in this example: " 'The sun is shining' means 'I'm biking' " Translated into a propositional formula the words become: "IF 'the sun is shining' THEN 'I'm biking', AND IF 'I'm biking' THEN 'the sun is shining'":<sup id="cite_ref-15" class="reference"><a href="#cite_note-15"><span class="cite-bracket">[</span>14<span class="cite-bracket">]</span></a></sup>

</p>

<dl><dd>"IF 's' THEN 'b' AND IF 'b' THEN 's' " is written as ((s → b) & (b → s)) or in an abbreviated form as (s ↔ b). As the rightmost symbol string is a <b>definition</b> for a new symbol in terms of the symbols on the left, the use of the IDENTITY sign = is appropriate:

<p>Different authors use different signs for logical equivalence: ↔ (e.g. Suppes, Goodstein, Hamilton), ≡ (e.g. Robbin), ⇔ (e.g. Bender and Williamson). Typically identity is written as the equals sign =. One exception to this rule is found in <i>Principia Mathematica</i>. For more about the philosophy of the notion of IDENTITY see <a href="Identity_of_indiscernibles" title="Identity of indiscernibles">Leibniz's law</a>.

</p><p>As noted above, Tarski considers IDENTITY to lie outside the propositional calculus, but he asserts that without the notion, "logic" is insufficient for mathematics and the deductive sciences. In fact the sign comes into the propositional calculus when a formula is to be evaluated.<sup id="cite_ref-16" class="reference"><a href="#cite_note-16"><span class="cite-bracket">[</span>15<span class="cite-bracket">]</span></a></sup>

</p><p>In some systems there are no truth tables, but rather just formal axioms (e.g. strings of symbols from a set { ~, →, (, ), variables p<sub>1</sub>, p<sub>2</sub>, p<sub>3</sub>, ... } and formula-formation rules (rules about how to make more symbol strings from previous strings by use of e.g. substitution and <a href="Modus_ponens" title="Modus ponens">modus ponens</a>). the result of such a calculus will be another formula (i.e. a well-formed symbol string). Eventually, however, if one wants to use the calculus to study notions of validity and truth, one must add axioms that define the behavior of the symbols called "the truth values" {T, F} ( or {1, 0}, etc.) relative to the other symbols.

</p><p>For example, Hamilton uses two symbols = and ≠ when he defines the notion of a <b>valuation v</b> of any <a href="Well-formed_formula" title="Well-formed formula">well-formed formulas</a> (wffs) <i>A</i> and <i>B</i> in his "formal statement calculus" L. A valuation <b>v</b> is a <i><a href="Function_(mathematics)" title="Function (mathematics)">function</a></i> from the wffs of his system L to the range (output) { T, F }, given that each variable p<sub>1</sub>, p<sub>2</sub>, p<sub>3</sub> in a wff is assigned an arbitrary truth value { T, F }.

</p>

/* start https://en.wikipedia.org/ */

.mw-parser-output table.numblk{border-collapse:collapse;border:none;margin-top:0;margin-right:0;margin-bottom:0}.mw-parser-output table.numblk>tbody>tr>td{vertical-align:middle;padding:0}.mw-parser-output table.numblk>tbody>tr>td:nth-child(2){width:99%}.mw-parser-output table.numblk>tbody>tr>td:nth-child(2)>table{border-collapse:collapse;margin:0;border:none;width:100%}.mw-parser-output table.numblk>tbody>tr>td:nth-child(2)>table>tbody>tr:first-child>td:first-child,.mw-parser-output table.numblk>tbody>tr>td:nth-child(2)>table>tbody>tr:first-child>td:last-child{padding:0 0.4ex}.mw-parser-output table.numblk>tbody>tr>td:nth-child(2)>table>tbody>tr:first-child>td:nth-child(2){width:100%;padding:0}.mw-parser-output table.numblk>tbody>tr>td:nth-child(2)>table>tbody>tr:last-child>td{padding:0}.mw-parser-output table.numblk>tbody>tr>td:last-child{font-weight:bold}.mw-parser-output table.numblk.numblk-raw-n>tbody>tr>td:last-child{font-weight:unset}.mw-parser-output table.numblk>tbody>tr>td:last-child::before{content:"("}.mw-parser-output table.numblk>tbody>tr>td:last-child::after{content:")"}.mw-parser-output table.numblk.numblk-raw-n>tbody>tr>td:last-child::before,.mw-parser-output table.numblk.numblk-raw-n>tbody>tr>td:last-child::after{content:none}.mw-parser-output table.numblk>tbody>tr>td{border:none}.mw-parser-output table.numblk.numblk-border>tbody>tr>td{border:thin solid}.mw-parser-output table.numblk>tbody>tr>td:nth-child(2)>table>tbody>tr:first-child>td{border:none}.mw-parser-output table.numblk.numblk-border>tbody>tr>td:nth-child(2)>table>tbody>tr:first-child>td{border:thin solid}.mw-parser-output table.numblk>tbody>tr>td:nth-child(2)>table>tbody>tr:last-child>td{border-left:none;border-right:none;border-bottom:none}.mw-parser-output table.numblk.numblk-border>tbody>tr>td:nth-child(2)>table>tbody>tr:last-child>td{border-left:thin solid;border-right:thin solid;border-bottom:thin solid}.mw-parser-output table.numblk:target{color:var(--color-base,#202122);background-color:#cfe8fd}@media screen{html.skin-theme-clientpref-night .mw-parser-output table.numblk:target{color:var(--color-base,#eaecf0);background-color:#301702}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output table.numblk:target{color:var(--color-base,#eaecf0);background-color:#301702}}

/* end https://en.wikipedia.org/ */

</style><table role="presentation" class="numblk" style="margin-left: 1.6em;"><tbody><tr><td class="nowrap"> <b>v</b>(<i>A</i>) ≠ <b>v</b>(~<i>A</i>)</td> <td></td> <td class="nowrap"><span id="math_i" class="reference nourlexpansion" style="font-weight:bold;">i</span></td></tr></tbody></table>

<p>The two definitions (<b><a href="#math_i">i</a></b>) and (<b><a href="#math_ii">ii</a></b>) define the equivalent of the truth tables for the ~ (NOT) and → (IMPLICATION) connectives of his system. The first one derives F ≠ T and T ≠ F, in other words " <b>v</b>(<i>A</i>) does not <b>mean</b> <b>v</b>(~<i>A</i>)". Definition (<b><a href="#math_ii">ii</a></b>) specifies the third row in the truth table, and the other three rows then come from an application of definition (<b><a href="#math_i">i</a></b>). In particular (<b><a href="#math_ii">ii</a></b>) <b>assigns</b> the value F (or a meaning of "F") to the entire expression. The definitions also serve as formation rules that allow substitution of a value previously derived into a formula:

</p>

<table>

</td>

</td>

<td style="background-color:#E5E0EC" width="50">v(A→B)

</td>

</td>

</td></tr>

<td height="12">(

</td>

<td>v(A)

</td>

<td style="background-color:#E5E0EC">→

</td>

<td>v(B)

</td>

<td>)

</td></tr>

</td>

<td>F

</td>

<td style="background-color:#E5E0EC">T

</td>

<td>F

</td>

<td>

</td></tr>

</td>

<td>F

</td>

<td style="background-color:#E5E0EC">T

</td>

<td>T

</td>

<td>

</td></tr>

</td>

<td>T

</td>

<td style="background-color:#CCC0DA">F

</td>

<td>F

</td>

<td>

</td></tr>

</td>

<td>T

</td>

<td style="background-color:#E5E0EC">T

</td>

<td>T

</td>

<td>

</td></tr></tbody></table>

<p>Some <a href="Formal_system" title="Formal system">formal systems</a> specify these valuation axioms at the outset in the form of certain formulas such as the <a href="Law_of_contradiction" class="mw-redirect" title="Law of contradiction">law of contradiction</a> or laws of identity and nullity. The choice of which ones to use, together with laws such as commutation and distribution, is up to the system's designer as long as the set of axioms is <b>complete</b> (i.e. sufficient to form and to evaluate any well-formed formula created in the system).

</p>

<div class="mw-heading mw-heading2"><h2 id="More_complex_formulas">More complex formulas</h2></div>

<p>As shown above, the CASE (IF c THEN b ELSE a ) connective is constructed either from the 2-argument connectives IF ... THEN ... and AND or from OR and AND and the 1-argument NOT. Connectives such as the n-argument AND (a & b & c & ... & n), OR (a ∨ b ∨ c ∨ ... ∨ n) are constructed from strings of two-argument AND and OR and written in abbreviated form without the parentheses. These, and other connectives as well, can then be used as building blocks for yet further connectives. Rhetoricians, philosophers, and mathematicians use truth tables and the various theorems to analyze and simplify their formulas.

</p><p>Electrical engineering uses drawn symbols and connect them with lines that stand for the mathematicals act of substitution and replacement. They then verify their drawings with truth tables and simplify the expressions as shown below by use of <a href="Karnaugh_map" title="Karnaugh map">Karnaugh maps</a> or the theorems. In this way engineers have created a host of "combinatorial logic" (i.e. connectives without feedback) such as "decoders", "encoders", "mutifunction gates", "majority logic", "binary adders", "arithmetic logic units", etc.

</p>

<div class="mw-heading mw-heading3"><h3 id="Definitions">Definitions</h3></div>

<p>A definition creates a new symbol and its behavior, often for the purposes of abbreviation. Once the definition is presented, either form of the equivalent symbol or formula can be used. The following symbolism =<sub>Df</sub> is following the convention of Reichenbach.<sup id="cite_ref-17" class="reference"><a href="#cite_note-17"><span class="cite-bracket">[</span>16<span class="cite-bracket">]</span></a></sup> Some examples of convenient definitions drawn from the symbol set { ~, &, (, ) } and variables. Each definition is producing a logically equivalent formula that can be used for substitution or replacement.

</p>

<dl><dd><ul><li>definition of a new variable: (c & d) =<sub>Df</sub> s</li>

<li>IMPLICATION: (~a ∨ b) =<sub>Df</sub> (a → b)</li>

<li>LOGICAL EQUIVALENCE: ( (a → b) & (b → a) ) =<sub>Df</sub> ( a ≡ b )</li></ul></dd></dl>

<div class="mw-heading mw-heading3"><h3 id="Axiom_and_definition_schemas">Axiom and definition <i>schemas</i></h3></div>

<p>The definitions above for OR, IMPLICATION, XOR, and logical equivalence are actually <a href="Axiom_schema" title="Axiom schema">schemas</a> (or "schemata"), that is, they are <i>models</i> (demonstrations, examples) for a general formula <i>format</i> but shown (for illustrative purposes) with specific letters a, b, c for the variables, whereas any variable letters can go in their places as long as the letter substitutions follow the rule of substitution below.

</p>

<dl><dd>Example: In the definition (~a ∨ b) =<sub>Df</sub> (a → b), other variable-symbols such as "SW2" and "CON1" might be used, i.e. formally:

<dl><dd>a =<sub>Df</sub> SW2, b =<sub>Df</sub> CON1, so we would have as an <i>instance</i> of the definition schema (~SW2 ∨ CON1) =<sub>Df</sub> (SW2 → CON1)</dd></dl></dd></dl>

<div class="mw-heading mw-heading3"><h3 id="Substitution_versus_replacement">Substitution versus replacement</h3></div>

<p><b>Substitution</b>: The variable or sub-formula to be substituted with another variable, constant, or sub-formula must be replaced in all instances throughout the overall formula.

</p>

<dl><dd>Example: (c & d) ∨ (p & ~(c & ~d)), but (q1 & ~q2) ≡ d. Now wherever variable "d" occurs, substitute (q<sub>1</sub> & ~q<sub>2</sub>):

<p><b>Replacement</b>: (i) the formula to be replaced must be within a tautology, i.e. <i>logically equivalent</i> ( connected by ≡ or ↔) to the formula that replaces it, and (ii) unlike substitution its permissible for the replacement to occur only in one place (i.e. for one formula).

</p>

<dl><dd>Example: Use this set of formula schemas/equivalences:

<dd><div><ol style="list-style-type:lower-alpha"><li>start with "a": a</li><li>Use 1 to replace "a" with (a ∨ 0): (a ∨ 0)</li><li>Use the notion of "schema" to substitute b for a in 2: ( (a & ~a) ≡ 0 )</li><li>Use 2 to replace 0 with (b & ~b): ( a ∨ (b & ~b) )</li><li>(see below for how to distribute "a ∨" over (b & ~b), etc.)</li></ol></div></dd></dl>

<div class="mw-heading mw-heading2"><h2 id="Inductive_definition">Inductive definition</h2></div>

<p>The classical presentation of propositional logic (see <a href="Herbert_Enderton" title="Herbert Enderton">Enderton</a> 2002) uses the connectives <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot ,\land ,\lor ,\to ,\leftrightarrow }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \lnot ,\land ,\lor ,\to ,\leftrightarrow }</annotation>

</semantics>

</math></span><img src="./f768b24786e436c7831132220a5b8affc1708203.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:13.434ex; height:2.343ex;" alt="{\displaystyle \lnot ,\land ,\lor ,\to ,\leftrightarrow }" loading="lazy"></span>. The set of formulas over a given set of propositional variables is <a href="Inductive_definition" class="mw-redirect" title="Inductive definition">inductively defined</a> to be the smallest set of expressions such that:

</p>

<ul><li>Each propositional variable in the set is a formula,</li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (\lnot \alpha )}</annotation>

</semantics>

</math></span><img src="./9c19b691174b3f3f58329842015a4eda18c622e8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.847ex; height:2.843ex;" alt="{\displaystyle (\lnot \alpha )}" loading="lazy"></span> is a formula whenever <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \alpha }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \alpha }</annotation>

</semantics>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (\alpha \,\Box \,\beta )}</annotation>

</semantics>

</math></span><img src="./6e55040aa75a26d46d1b7916a2669b466d4bf7a5.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:7.211ex; height:2.843ex;" alt="{\displaystyle (\alpha \,\Box \,\beta )}" loading="lazy"></span> is a formula whenever <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \alpha }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \alpha }</annotation>

</semantics>

</math></span><img src="./b79333175c8b3f0840bfb4ec41b8072c83ea88d3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.488ex; height:1.676ex;" alt="{\displaystyle \alpha }" loading="lazy"></span> and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \beta }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \beta }</annotation>

</semantics>

</math></span><img src="./7ed48a5e36207156fb792fa79d29925d2f7901e8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.332ex; height:2.509ex;" alt="{\displaystyle \beta }" loading="lazy"></span> are formulas and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Box }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \Box }</annotation>

</semantics>

</math></span><img src="./029b77f09ebeaf7528fc831fe57848be51f2240b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.808ex; height:2.176ex;" alt="{\displaystyle \Box }" loading="lazy"></span> is one of the binary connectives <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \land ,\lor ,\to ,\leftrightarrow }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \land ,\lor ,\to ,\leftrightarrow }</annotation>

</semantics>

<p>This inductive definition can be easily extended to cover additional connectives.

</p><p>The inductive definition can also be rephrased in terms of a <a href="Closure_(mathematics)" title="Closure (mathematics)">closure</a> operation (Enderton 2002). Let <i>V</i> denote a set of propositional variables and let <i>X<sub>V</sub></i> denote the set of all strings from an alphabet including symbols in <i>V</i>, left and right parentheses, and all the logical connectives under consideration. Each logical connective corresponds to a formula building operation, a function from <i>XX<sub>V</sub></i> to <i>XX<sub>V</sub></i>:

</p>

<ul><li>Given a string <i>z</i>, the operation <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {E}}_{\lnot }(z)}">

<msub>

</mrow>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {E}}_{\lnot }(z)}</annotation>

</semantics>

</math></span><img src="./97e157de2d09945136a30322464a7baa93e6bcd8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:5.453ex; height:2.843ex;" alt="{\displaystyle {\mathcal {E}}_{\lnot }(z)}" loading="lazy"></span> returns <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (\lnot z)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (\lnot z)}</annotation>

</semantics>

</math></span><img src="./9b0eebedbd45f600919bd17f6d8caae791fcb27d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.448ex; height:2.843ex;" alt="{\displaystyle (\lnot z)}" loading="lazy"></span>.</li>

<li>Given strings <i>y</i> and <i>z</i>, the operation <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {E}}_{\land }(y,z)}">

<msub>

</mrow>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {E}}_{\land }(y,z)}</annotation>

</semantics>

</math></span><img src="./882188047afe445e0647726897f31aaa2188f1c4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:7.643ex; height:2.843ex;" alt="{\displaystyle {\mathcal {E}}_{\land }(y,z)}" loading="lazy"></span> returns <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (y\land z)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (y\land z)}</annotation>

</semantics>

</math></span><img src="./b22b0e91cf9a3e138885ba87c1f4a2ed1162a128.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:6.636ex; height:2.843ex;" alt="{\displaystyle (y\land z)}" loading="lazy"></span>. There are similar operations <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {E}}_{\lor }}">

<msub>

</mrow>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {E}}_{\lor }}</annotation>

</semantics>

</math></span><img src="./0bca9bf5dce3883566f6250da7bc52713a5083d7.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.556ex; height:2.509ex;" alt="{\displaystyle {\mathcal {E}}_{\lor }}" loading="lazy"></span>, <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {E}}_{\to }}">

<msub>

</mrow>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {E}}_{\to }}</annotation>

</semantics>

</math></span><img src="./51a656efd1b6bc292138bbd57ca36107bb823e9c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.103ex; height:2.509ex;" alt="{\displaystyle {\mathcal {E}}_{\to }}" loading="lazy"></span>, and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {E}}_{\leftrightarrow }}">

<msub>

</mrow>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {E}}_{\leftrightarrow }}</annotation>

</semantics>

</math></span><img src="./30995ab56adc06d7b90e52062f6e0cb495316180.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.103ex; height:2.509ex;" alt="{\displaystyle {\mathcal {E}}_{\leftrightarrow }}" loading="lazy"></span> corresponding to the other binary connectives.</li></ul>

<p>The set of formulas over <i>V</i> is defined to be the smallest subset of <i>XX<sub>V</sub></i> containing <i>V</i> and closed under all the formula building operations.

</p>

<div class="mw-heading mw-heading2"><h2 id="Parsing_formulas">Parsing formulas</h2></div>

<p>The following "laws" of the propositional calculus are used to "reduce" complex formulas. The "laws" can be verified easily with truth tables. For each law, the principal (outermost) connective is associated with logical equivalence ≡ or identity =. A complete analysis of all 2<sup>n</sup> combinations of truth-values for its <i>n</i> distinct variables will result in a column of 1's (T's) underneath this connective. This finding makes each law, by definition, a tautology. And, for a given law, because its formula on the left and right are equivalent (or identical) they can be substituted for one another.

</p>

<ul><li>Example: The following truth table is De Morgan's law for the behavior of NOT over OR: ~(a ∨ b) ≡ (~a & ~b). To the left of the principal connective ≡ (yellow column labelled "taut") the formula ~(b ∨ a) evaluates to (1, 0, 0, 0) under the label "P". On the right of "taut" the formula (~(b) ∨ ~(a)) also evaluates to (1, 0, 0, 0) under the label "Q". As the two columns have equivalent evaluations, the logical equivalence ≡ under "taut" evaluates to (1, 1, 1, 1), i.e. P ≡ Q. Thus either formula can be substituted for the other if it appears in a larger formula.</li></ul>

</td>

</td>

</td>

</td>

<td style="background-color:#D7E4BC" width="10.5">P

</td>

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#FFFF99" width="21.75">taut

</td>

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#DBE5F1" width="12.75">Q

</td>

</td>

</td>

</td>

</td>

</td>

</td></tr>

<td style="font-size:9pt" height="15">b

</td>

<td style="font-size:9pt">a

</td>

</td>

<td style="font-size:9pt">(

</td>

<td style="background-color:#D7E4BC;font-size:9pt">~

</td>

<td style="font-size:9pt">(

</td>

<td style="font-size:9pt">b

</td>

<td style="background-color:#FDE9D9;font-size:9pt">V

</td>

<td style="font-size:9pt">a

</td>

<td style="font-size:9pt">)

</td>

<td style="background-color:#FFFF99">≡

</td>

<td style="font-size:9pt">(

</td>

<td style="background-color:#EAF1DD;font-size:9pt">~

</td>

<td style="font-size:9pt">(

</td>

<td style="font-size:9pt">b

</td>

<td style="font-size:9pt">)

</td>

<td style="background-color:#DBE5F1;font-size:9pt">&

</td>

<td style="background-color:#EAF1DD;font-size:9pt">~

</td>

<td style="font-size:9pt">(

</td>

<td style="font-size:9pt">a

</td>

<td style="font-size:9pt">)

</td>

<td style="font-size:9pt">)

</td>

<td style="font-size:9pt">)

</td></tr>

<td height="12">0

</td>

<td>0

</td>

</td>

<td>

</td>

<td style="background-color:#D7E4BC">1

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#FFFF99">1

</td>

<td>

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#DBE5F1">1

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td>

</td></tr>

<td height="12">0

</td>

<td>1

</td>

</td>

<td>

</td>

<td style="background-color:#D7E4BC">0

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#FFFF99">1

</td>

<td>

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#EAF1DD">0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>

</td>

<td>

</td></tr>

<td height="12">1

</td>

<td>0

</td>

</td>

<td>

</td>

<td style="background-color:#D7E4BC">0

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#FFFF99">1

</td>

<td>

</td>

<td style="background-color:#EAF1DD">0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td>

</td></tr>

<td height="12">1

</td>

<td>1

</td>

</td>

<td>

</td>

<td style="background-color:#D7E4BC">0

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#FFFF99">1

</td>

<td>

</td>

<td style="background-color:#EAF1DD">0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#EAF1DD">0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>

</td>

<td>

</td></tr></tbody></table>

<p>Enterprising readers might challenge themselves to invent an "axiomatic system" that uses the symbols { ∨, &, ~, (, ), variables a, b, c }, the formation rules specified above, and as few as possible of the laws listed below, and then derive as theorems the others as well as the truth-table valuations for ∨, &, and ~. One set attributed to Huntington (1904) (Suppes:204) uses eight of the laws defined below.

</p><p>If used in an axiomatic system, the symbols 1 and 0 (or T and F) are considered to be well-formed formulas and thus obey all the same rules as the variables. Thus the laws listed below are actually <a href="Axiom_schema" title="Axiom schema">axiom schemas</a>, that is, they stand in place of an infinite number of instances. Thus ( x ∨ y ) ≡ ( y ∨ x ) might be used in one instance, ( p ∨ 0 ) ≡ ( 0 ∨ p ) and in another instance ( 1 ∨ q ) ≡ ( q ∨ 1 ), etc.

</p>

<div class="mw-heading mw-heading3"><h3 id="Connective_seniority_(symbol_rank)">Connective seniority (symbol rank)</h3></div>

<p>In general, to avoid confusion during analysis and evaluation of propositional formulas, one can make liberal use of parentheses. However, quite often authors leave them out. To parse a complicated formula one first needs to know the seniority, or rank, that each of the connectives (excepting *) has over the other connectives. To "well-form" a formula, start with the connective with the highest rank and add parentheses around its components, then move down in rank (paying close attention to the connective's scope over which it is working). From most- to least-senior, with the predicate signs ∀x and ∃x, the IDENTITY = and arithmetic signs added for completeness:<sup id="cite_ref-19" class="reference"><a href="#cite_note-19"><span class="cite-bracket">[</span>b<span class="cite-bracket">]</span></a></sup>

</p>

<dd>(LOGICAL EQUIVALENCE)</dd>

<dd>(IMPLICATION)</dd>

<dd>(THERE EXISTS AN x)</dd>

<dd>(IDENTITY)</dd>

<dd>(arithmetic sum)</dd>

<dd>(arithmetic multiply)</dd>

<dd>(s, arithmetic successor).</dd></dl></dd></dl>

<p>Thus the formula can be parsed—but because NOT does not obey the distributive law, the parentheses around the inner formula (~c & ~d) is mandatory:

</p>

<dl><dd>Example: " d & c ∨ w " rewritten is ( (d & c) ∨ w )</dd>

<dd>Example: " a & a → b ≡ a & ~a ∨ b " rewritten (rigorously) is

<dl><dd><ul><li>≡ has seniority: ( ( a & a → b ) ≡ ( a & ~a ∨ b ) )</li>

<li>→ has seniority: ( ( a & (a → b) ) ≡ ( a & ~a ∨ b ) )</li>

<li>& has seniority both sides: ( ( ( (a) & (a → b) ) ) ≡ ( ( (a) & (~a ∨ b) ) )</li>

<li>~ has seniority: ( ( ( (a) & (a → b) ) ) ≡ ( ( (a) & (~(a) ∨ b) ) )</li>

<li>check 9 ( -parenthesis and 9 ) -parenthesis: ( ( ( (a) & (a → b) ) ) ≡ ( ( (a) & (~(a) ∨ b) ) )</li></ul></dd></dl></dd>

<dd>Example:

<dl><dd>d & c ∨ p & ~(c & ~d) ≡ c & d ∨ p & c ∨ p & ~d rewritten is ( ( (d & c) ∨ ( p & ~((c & ~(d)) ) ) ) ≡ ( (c & d) ∨ (p & c) ∨ (p & ~(d)) ) )</dd></dl></dd></dl>

<div class="mw-heading mw-heading3"><h3 id="Commutative_and_associative_laws">Commutative and associative laws</h3></div>

<p>Both AND and OR obey the <a href="Commutative_law" class="mw-redirect" title="Commutative law">commutative law</a> and <a href="Associative_law" class="mw-redirect" title="Associative law">associative law</a>:

</p>

<ul><li>Commutative law for OR: ( a ∨ b ) ≡ ( b ∨ a )</li>

<li>Commutative law for AND: ( a & b ) ≡ ( b & a )</li>

<li>Associative law for OR: (( a ∨ b ) ∨ c ) ≡ ( a ∨ (b ∨ c) )</li>

<li>Associative law for AND: (( a & b ) & c ) ≡ ( a & (b & c) )</li></ul>

<p><b>Omitting parentheses in strings of AND and OR</b>: The connectives are considered to be unary (one-variable, e.g. NOT) and binary (i.e. two-variable AND, OR, IMPLIES). For example:

</p>

<dl><dd>( (c & d) ∨ (p & c) ∨ (p & ~d) ) above should be written ( ((c & d) ∨ (p & c)) ∨ (p & ~(d) ) ) or possibly ( (c & d) ∨ ( (p & c) ∨ (p & ~(d)) ) )</dd></dl>

<p>However, a truth-table demonstration shows that the form without the extra parentheses is perfectly adequate.

</p><p><b>Omitting parentheses with regards to a single-variable NOT</b>: While ~(a) where a is a single variable is perfectly clear, ~a is adequate and is the usual way this <a href="Literal_(mathematical_logic)" title="Literal (mathematical logic)">literal</a> would appear. When the NOT is over a formula with more than one symbol, then the parentheses are mandatory, e.g. ~(a ∨ b).

</p>

<div class="mw-heading mw-heading3"><h3 id="Distributive_laws">Distributive laws</h3></div>

<p>OR distributes over AND and AND distributes over OR. NOT does not distribute over AND or OR. See below about De Morgan's law:

</p>

<ul><li>Distributive law for OR: ( c ∨ ( a & b) ) ≡ ( (c ∨ a) & (c ∨ b) )</li>

<li>Distributive law for AND: ( c & ( a ∨ b) ) ≡ ( (c & a) ∨ (c & b) )</li></ul>

<div class="mw-heading mw-heading3"><h3 id="De_Morgan's_laws">De Morgan's laws</h3></div>

<p>NOT, when distributed over OR or AND, does something peculiar (again, these can be verified with a truth-table):

</p>

<ul><li>De Morgan's law for OR: ¬(a ∨ b) ≡ (¬a ^ ¬b)</li>

<li>De Morgan's law for AND: ¬(a ^ b) ≡ (¬a ∨ ¬b)</li></ul>

<div class="mw-heading mw-heading3"><h3 id="Laws_of_absorption">Laws of absorption</h3></div>

<p>Absorption, in particular the first one, causes the "laws" of logic to differ from the "laws" of arithmetic:

</p>

<ul><li>Absorption (idempotency) for OR: (a ∨ a) ≡ a</li>

<li>Absorption (idempotency) for AND: (a & a) ≡ a</li></ul>

<div class="mw-heading mw-heading3"><h3 id="Laws_of_evaluation:_Identity,_nullity,_and_complement">Laws of evaluation: Identity, nullity, and complement</h3></div>

<p>The sign " = " (as distinguished from logical equivalence ≡, alternately ↔ or ⇔) symbolizes the assignment of value or meaning. Thus the string (a & ~(a)) symbolizes "0", i.e. it means the same thing as symbol "0" ". In some "systems" this will be an axiom (definition) perhaps shown as ( (a & ~(a)) =<sub>Df</sub> 0 ); in other systems, it may be derived in the truth table below:

</p>

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#C5D9F1" width="10.5">c

</td>

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#FFFF99" width="18">taut

</td>

<td width="13.5">c

</td>

</td></tr>

<td style="font-size:9pt" height="15">a

</td>

</td>

<td style="font-size:9pt">(

</td>

<td style="font-size:9pt">(

</td>

<td style="font-size:9pt">a

</td>

<td style="background-color:#C5D9F1;font-size:9pt">&

</td>

<td style="background-color:#EAF1DD;font-size:9pt">~

</td>

<td style="font-size:9pt">(

</td>

<td style="font-size:9pt">a

</td>

<td style="font-size:9pt">)

</td>

<td style="font-size:9pt">)

</td>

<td style="background-color:#FFFF99">≡

</td>

<td style="font-size:9pt">0

</td>

<td style="font-size:9pt">)

</td></tr>

<td height="12">0

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#C5D9F1">0

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#FFFF99">1

</td>

<td>0

</td>

<td>

</td></tr>

<td height="12">1

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#C5D9F1">0

</td>

<td style="background-color:#EAF1DD">0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#FFFF99">1

</td>

<td>0

</td>

<td>

</td></tr></tbody></table>

<ul><li>Commutation of equality: (a = b) ≡ (b = a)</li>

<li>Identity for OR: (a ∨ 0) = a or (a ∨ F) = a</li>

<li>Identity for AND: (a & 1) = a or (a & T) = a</li>

<li>Nullity for OR: (a ∨ 1) = 1 or (a ∨ T) = T</li>

<li>Nullity for AND: (a & 0) = 0 or (a & F) = F</li>

<li>Complement for OR: (a ∨ ~a) = 1 or (a ∨ ~a) = T, <a href="Law_of_excluded_middle" title="Law of excluded middle">law of excluded middle</a></li>

<li>Complement for AND: (a & ~a) = 0 or (a & ~a) = F, <a href="Law_of_contradiction" class="mw-redirect" title="Law of contradiction">law of contradiction</a></li></ul>

<div class="mw-heading mw-heading3"><h3 id="Double_negative_(involution)">Double negative (involution)</h3></div>

<div class="mw-heading mw-heading2"><h2 id="Well-formed_formulas_(wffs)">Well-formed formulas (wffs)</h2></div>

<p>A key property of formulas is that they can be uniquely parsed to determine the structure of the formula in terms of its propositional variables and logical connectives. When formulas are written in <a href="Infix_notation" title="Infix notation">infix notation</a>, as above, unique readability is ensured through an appropriate use of parentheses in the definition of formulas. Alternatively, formulas can be written in <a href="Polish_notation" title="Polish notation">Polish notation</a> or <a href="Reverse_Polish_notation" title="Reverse Polish notation">reverse Polish notation</a>, eliminating the need for parentheses altogether.

</p><p>The inductive definition of infix formulas in the previous section can be converted to a <a href="Formal_grammar" title="Formal grammar">formal grammar</a> in <a href="Backus-Naur_form" class="mw-redirect" title="Backus-Naur form">Backus-Naur form</a>:

</p>

<div class="mw-highlight mw-highlight-lang-bnf mw-content-ltr" dir="ltr"><pre><span class="p"><</span><span class="nc">formula</span><span class="p">></span> <span class="o">::=</span> <span class="p"><</span><span class="nc">propositional variable</span><span class="p">></span>

| ( ¬ <span class="p"><</span><span class="nc">formula</span><span class="p">></span> )

| ( <span class="p"><</span><span class="nc">formula</span><span class="p">></span> ∧ <span class="p"><</span><span class="nc">formula</span><span class="p">></span>)

| ( <span class="p"><</span><span class="nc">formula</span><span class="p">></span> ∨ <span class="p"><</span><span class="nc">formula</span><span class="p">></span> )

| ( <span class="p"><</span><span class="nc">formula</span><span class="p">></span> → <span class="p"><</span><span class="nc">formula</span><span class="p">></span> )

| ( <span class="p"><</span><span class="nc">formula</span><span class="p">></span> ↔ <span class="p"><</span><span class="nc">formula</span><span class="p">></span> )

</pre></div>

<p>It can be shown that any expression matched by the grammar has a balanced number of left and right parentheses, and any nonempty initial segment of a formula has more left than right parentheses.<sup id="cite_ref-20" class="reference"><a href="#cite_note-20"><span class="cite-bracket">[</span>18<span class="cite-bracket">]</span></a></sup> This fact can be used to give an algorithm for parsing formulas. For example, suppose that an expression <i>x</i> begins with <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (\lnot }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (\lnot }</annotation>

</semantics>

</math></span><img src="./610f9ee024f577dc96267e5dcd9bf9219b6d3a06.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:2.455ex; height:2.843ex;" alt="{\displaystyle (\lnot }" loading="lazy"></span>. Starting after the second symbol, match the shortest subexpression <i>y</i> of <i>x</i> that has balanced parentheses. If <i>x</i> is a formula, there is exactly one symbol left after this expression, this symbol is a closing parenthesis, and <i>y</i> itself is a formula. This idea can be used to generate a <a href="Recursive_descent_parser" title="Recursive descent parser">recursive descent parser</a> for formulas.

</p><p><b>Example of parenthesis counting</b>:

</p><p>This method locates as "1" the <b>principal connective</b> — the connective under which the overall evaluation of the formula occurs for the outer-most parentheses (which are often omitted).<sup id="cite_ref-21" class="reference"><a href="#cite_note-21"><span class="cite-bracket">[</span>19<span class="cite-bracket">]</span></a></sup> It also locates the inner-most connective where one would begin evaluatation of the formula without the use of a truth table, e.g. at "level 6".

</p>

</td>

<th width="27.75">start

</th>

<td style="background-color:#99FF99" width="12">(

</td>

<td style="background-color:#99FF99" width="12">(

</td>

<td style="background-color:#99FF99" width="12">(

</td>

<td width="12">c

</td>

<td width="12">&

</td>

<td width="12">d

</td>

<td style="background-color:#FFC000" width="12">)

</td>

<td width="12">V

</td>

<td style="background-color:#99FF99" width="12">(

</td>

<td width="12">p

</td>

<td width="12">&

</td>

<td width="12">~

</td>

<td style="background-color:#99FF99" width="12">(

</td>

<td style="background-color:#99FF99" width="12">(

</td>

<td width="12">c

</td>

<td width="12">&

</td>

<td width="12">~

</td>

<td style="background-color:#99FF99" width="12">(

</td>

<td width="12">d

</td>

<td style="background-color:#FFC000" width="12">)

</td>

<td style="background-color:#FFC000" width="12">)

</td>

<td style="background-color:#FFC000" width="12">)

</td>

<td style="background-color:#FFC000" width="12">)

</td>

<td style="background-color:#FFC000" width="12">)

</td>

<td width="12">=

</td>

<td style="background-color:#99FF99" width="12">(

</td>

<td style="background-color:#99FF99" width="12">(

</td>

<td style="background-color:#99FF99" width="12">(

</td>

<td width="12">c

</td>

<td width="12">&

</td>

<td width="12">d

</td>

<td style="background-color:#FFC000" width="12">)

</td>

<td width="12">V

</td>

<td style="background-color:#99FF99" width="12">(

</td>

<td width="12">p

</td>

<td width="12">&

</td>

<td width="12">d

</td>

<td style="background-color:#FFC000" width="12">)

</td>

<td style="background-color:#FFC000" width="12">)

</td>

<td width="12">V

</td>

<td style="background-color:#99FF99" width="12">(

</td>

<td width="12">p

</td>

<td width="12">&

</td>

<td width="12">~

</td>

<td style="background-color:#99FF99" width="12">(

</td>

<td width="12">c

</td>

<td style="background-color:#FFC000" width="12">)

</td>

<td style="background-color:#FFC000" width="12">)

</td>

<td style="background-color:#FFC000" width="12">)

</td>

<td style="background-color:#FFC000" width="12">)

</td></tr>

<th height="13.5" align="right" valign="bottom">count

</th>

<td align="center" valign="bottom">0

</td>

<td style="background-color:#99FF99" align="center" valign="bottom">1

</td>

<td style="background-color:#99FF99" align="center" valign="bottom">2

</td>

<td style="background-color:#99FF99" align="center" valign="bottom">3

</td>

<td align="center" valign="bottom">3

</td>

<td align="center" valign="bottom">3

</td>

<td align="center" valign="bottom">3

</td>

<td style="background-color:#FFC000" align="center" valign="bottom">2

</td>

<td align="center" valign="bottom">2

</td>

<td style="background-color:#99FF99" align="center" valign="bottom">3

</td>

<td align="center" valign="bottom">3

</td>

<td align="center" valign="bottom">3

</td>

<td align="center" valign="bottom">3

</td>

<td style="background-color:#99FF99" align="center" valign="bottom">4

</td>

<td style="background-color:#99FF99" align="center" valign="bottom">5

</td>

<td align="center" valign="bottom">5

</td>

<td align="center" valign="bottom">5

</td>

<td align="center" valign="bottom">5

</td>

<td style="background-color:#99FF99;font-weight:bold" align="center" valign="bottom">6

</td>

<td align="center" valign="bottom">6

</td>

<td style="background-color:#FFC000" align="center" valign="bottom">5

</td>

<td style="background-color:#FFC000" align="center" valign="bottom">4

</td>

<td style="background-color:#FFC000" align="center" valign="bottom">3

</td>

<td style="background-color:#FFC000" align="center" valign="bottom">3

</td>

<td style="background-color:#FFC000" align="center" valign="bottom">1

</td>

<td align="center" valign="bottom">1

</td>

<td style="background-color:#99FF99" align="center" valign="bottom">2

</td>

<td style="background-color:#99FF99" align="center" valign="bottom">3

</td>

<td style="background-color:#99FF99" align="center" valign="bottom">4

</td>

<td align="center" valign="bottom">4

</td>

<td align="center" valign="bottom">4

</td>

<td align="center" valign="bottom">4

</td>

<td style="background-color:#FFC000" align="center" valign="bottom">3

</td>

<td align="center" valign="bottom">3

</td>

<td style="background-color:#99FF99" align="center" valign="bottom">4

</td>

<td align="center" valign="bottom">4

</td>

<td align="center" valign="bottom">4

</td>

<td align="center" valign="bottom">4

</td>

<td style="background-color:#FFC000" align="center" valign="bottom">3

</td>

<td style="background-color:#FFC000" align="center" valign="bottom">2

</td>

<td align="center" valign="bottom">2

</td>

<td style="background-color:#99FF99" align="center" valign="bottom">3

</td>

<td align="center" valign="bottom">3

</td>

<td align="center" valign="bottom">3

</td>

<td align="center" valign="bottom">3

</td>

<td style="background-color:#99FF99" align="center" valign="bottom">3

</td>

<td align="center" valign="bottom">3

</td>

<td style="background-color:#FFC000" align="center" valign="bottom">3

</td>

<td style="background-color:#FFC000" align="center" valign="bottom">2

</td>

<td style="background-color:#FFC000" align="center" valign="bottom">1

</td>

<td style="background-color:#FFC000" align="center" valign="bottom">0

</td></tr></tbody></table>

<div class="mw-heading mw-heading3"><h3 id="Well-formed_formulas_versus_valid_formulas_in_inferences">Well-formed formulas versus valid formulas in inferences</h3></div>

<p>The notion of valid argument is usually applied to <a href="Inference" title="Inference">inferences</a> in arguments, but arguments reduce to propositional formulas and can be evaluated the same as any other propositional formula. Here a valid inference means: "The formula that represents the inference evaluates to "truth" beneath its principal connective, no matter what truth-values are assigned to its variables", i.e. the formula is a tautology.<sup id="cite_ref-22" class="reference"><a href="#cite_note-22"><span class="cite-bracket">[</span>20<span class="cite-bracket">]</span></a></sup>

Quite possibly a formula will be <i>well-formed</i> but not valid. Another way of saying this is: "Being well-formed is <i>necessary</i> for a formula to be valid but it is not <i>sufficient</i>." The only way to find out if it is <i>both</i> well-formed <i>and</i> valid is to submit it to verification with a truth table or by use of the "laws":

</p>

<ul><li>Example 1: What does one make of the following difficult-to-follow assertion? Is it valid? "If it's sunny, but if the frog is croaking then it's not sunny, then it's the same as saying that the frog isn't croaking." Convert this to a propositional formula as follows:

<dl><dd><dl><dd>" IF (a AND (IF b THEN NOT-a) THEN NOT-a" where " a " represents "its sunny" and " b " represents "the frog is croaking":</dd>

<dd>This is well-formed, but is it <i>valid</i>? In other words, when evaluated will this yield a tautology (all T) beneath the logical-equivalence symbol ≡ ? The answer is NO, it is not valid. However, if reconstructed as an <i>implication</i> then the argument <i>is</i> valid.</dd>

<dd>"Saying it's sunny, but if the frog is croaking then it's not sunny, <i>implies</i> that the frog isn't croaking."</dd>

<dd>Other circumstances may be preventing the frog from croaking: perhaps a crane ate it.</dd></dl></li>

<li>Example 2 (from Reichenbach via Bertrand Russell):

<dl><dd>"If pigs have wings, some winged animals are good to eat. Some winged animals are good to eat, so pigs have wings."</dd>

<dd>( ((a) → (b)) & (b) → (a) ) is well formed, but an invalid argument as shown by the red evaluation under the principal implication:</dd></dl></li></ul>

<td width="18.75" height="12">W

</td>

<td width="18.75">G

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#CCC0DA" width="19.5">arg

</td>

</td>

</td></tr>

<td style="font-size:9pt" height="12.75">a

</td>

<td style="font-size:9pt">b

</td>

</td>

<td style="font-size:9pt">(

</td>

<td style="font-size:9pt">(

</td>

<td style="font-size:9pt">(

</td>

<td style="font-size:9pt">a

</td>

</td>

<td style="font-size:9pt">b

</td>

<td style="font-size:9pt">)

</td>

<td style="background-color:#DBE5F1">&

</td>

<td style="font-size:9pt">b

</td>

<td style="font-size:9pt">)

</td>

</td>

<td style="font-size:9pt">a

</td>

<td style="font-size:9pt">)

</td></tr>

<td height="12">0

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#F2DDDC">1

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#CCC0DA">1

</td>

<td>0

</td>

<td>

</td></tr>

<td height="12">0

</td>

<td>1

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#F2DDDC">1

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#DBE5F1">1

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:red">0

</td>

<td>0

</td>

<td>

</td></tr>

<td height="12">1

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#F2DDDC">0

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#CCC0DA">1

</td>

<td>1

</td>

<td>

</td></tr>

<td height="12">1

</td>

<td>1

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#F2DDDC">1

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#DBE5F1">1

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#CCC0DA">1

</td>

<td>1

</td>

<td>

</td></tr></tbody></table>

<div class="mw-heading mw-heading2"><h2 id="Reduced_sets_of_connectives">Reduced sets of connectives</h2></div>

<p>A set of logical connectives is called complete if every propositional formula is tautologically equivalent to a formula with just the connectives in that set. There are many complete sets of connectives, including <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \{\land ,\lnot \}}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \{\land ,\lnot \}}</annotation>

</semantics>

</math></span><img src="./abafd3bfc91ad6fbbde79afba535eb3e615f95f3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:6.46ex; height:2.843ex;" alt="{\displaystyle \{\land ,\lnot \}}" loading="lazy"></span>, <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \{\lor ,\lnot \}}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \{\lor ,\lnot \}}</annotation>

</semantics>

</math></span><img src="./7421f5ba05cb6e9d201b88eb9990c7b5abb26f12.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:6.46ex; height:2.843ex;" alt="{\displaystyle \{\lor ,\lnot \}}" loading="lazy"></span>, and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \{\to ,\lnot \}}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \{\to ,\lnot \}}</annotation>

</semantics>

</math></span><img src="./a0d449bb0d656534b8a02eed3e3a58db7a521971.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:7.233ex; height:2.843ex;" alt="{\displaystyle \{\to ,\lnot \}}" loading="lazy"></span>. There are two binary connectives that are complete on their own, corresponding to NAND and NOR, respectively.<sup id="cite_ref-23" class="reference"><a href="#cite_note-23"><span class="cite-bracket">[</span>21<span class="cite-bracket">]</span></a></sup> Some pairs are not complete, for example <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \{\land ,\lor \}}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \{\land ,\lor \}}</annotation>

</semantics>

</math></span><img src="./164b435f78429eeb8b098ba5e13e905937257764.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:6.46ex; height:2.843ex;" alt="{\displaystyle \{\land ,\lor \}}" loading="lazy"></span>.

</p>

<div class="mw-heading mw-heading3"><h3 id="The_stroke_(NAND)">The stroke (NAND)</h3></div>

<p>The binary connective corresponding to NAND is called the <a href="Sheffer_stroke" title="Sheffer stroke">Sheffer stroke</a>, and written with a vertical bar | or vertical arrow ↑. The completeness of this connective was noted in <i>Principia Mathematica</i> (1927:xvii). Since it is complete on its own, all other connectives can be expressed using only the stroke. For example, where the symbol " ≡ " represents <i>logical equivalence</i>:

</p>

<p>In particular, the zero-ary connectives <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \top }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \top }</annotation>

</semantics>

</math></span><img src="./cf12e436fef2365e76fcb1034a51179d8328bb33.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.808ex; height:2.176ex;" alt="{\displaystyle \top }" loading="lazy"></span> (representing truth) and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \bot }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \bot }</annotation>

</semantics>

</p>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \top \equiv (a|(a|a))}</annotation>

</semantics>

</math></span><img src="./5ea3fb00f11d46dc290b4bf268e2c1e1fb41126b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:13.508ex; height:2.843ex;" alt="{\displaystyle \top \equiv (a|(a|a))}" loading="lazy"></span></dd>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \bot \equiv (\top |\top )}</annotation>

</semantics>

</math></span><img src="./538e32789a212767c5116fec049eceee339de505.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:10.979ex; height:2.843ex;" alt="{\displaystyle \bot \equiv (\top |\top )}" loading="lazy"></span></dd></dl>

<p>This connective together with { 0, 1 }, ( or { F, T } or { <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \bot }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \bot }</annotation>

</semantics>

</math></span><img src="./f282c7bc331cc3bfcf1c57f1452cc23c022f58de.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.808ex; height:2.176ex;" alt="{\displaystyle \bot }" loading="lazy"></span>, <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \top }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \top }</annotation>

</semantics>

</math></span><img src="./cf12e436fef2365e76fcb1034a51179d8328bb33.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.808ex; height:2.176ex;" alt="{\displaystyle \top }" loading="lazy"></span> } ) forms a complete set. In the following the IF...THEN...ELSE <a href="Relation_(mathematics)" title="Relation (mathematics)">relation</a> (c, b, a) = d represents ( (c → b) ∨ (~c → a) ) ≡ ( (c & b) ∨ (~c & a) ) = d

</p>

<p>Example: The following shows how a theorem-based proof of "(c, b, 1) ≡ (c → b)" would proceed, below the proof is its truth-table verification. ( Note: (c → b) is <i>defined</i> to be (~c ∨ b) ):

</p>

<dl><dd><ul><li>Begin with the reduced form: ( (c & b) ∨ (~c & a) )</li>

<li>Substitute "1" for a: ( (c & b) ∨ (~c & 1) )</li>

<li>Identity (~c & 1) = ~c: ( (c & b) ∨ (~c) )</li>

<li>Law of commutation for V: ( (~c) ∨ (c & b) )</li>

<li>Distribute "~c V" over (c & b): ( ((~c) ∨ c ) & ((~c) ∨ b )</li>

<li>Law of excluded middle (((~c) ∨ c ) = 1 ): ( (1) & ((~c) ∨ b ) )</li>

<li>Distribute "(1) &" over ((~c) ∨ b): ( ((1) & (~c)) ∨ ((1) & b )) )</li>

<li>Commutivity and Identity (( 1 & ~c) = (~c & 1) = ~c, and (( 1 & b) ≡ (b & 1) ≡ b: ( ~c ∨ b )</li>

<li>( ~c ∨ b ) is defined as <b>c → b</b> Q. E. D.</li></ul></dd></dl>

<p>In the following truth table the column labelled "taut" for tautology evaluates logical equivalence (symbolized here by ≡) between the two columns labelled d. Because all four rows under "taut" are 1's, the equivalence indeed represents a tautology.

</p>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#FDE9D9" width="11.25">d

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#DDD9C3" width="19.5">taut

</td>

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#FDE9D9" width="11.25">d

</td>

</td>

</td>

</td></tr>

<td style="background-color:#F2F2F2" height="12">rows

</td>

<td>c

</td>

<td>b

</td>

<td>a

</td>

</td>

<td>(

</td>

<td>(

</td>

<td>(

</td>

<td>c

</td>

<td style="background-color:#DBE5F1">&

</td>

<td>b

</td>

<td>)

</td>

<td style="background-color:#FDE9D9">V

</td>

<td>(

</td>

<td style="background-color:#EAF1DD">~

</td>

<td>(

</td>

<td>c

</td>

<td>)

</td>

<td style="background-color:#DBE5F1">&

</td>

<td>a

</td>

<td>)

</td>

<td>)

</td>

<td style="background-color:#DDD9C3">≡

</td>

<td>(

</td>

<td style="background-color:#EAF1DD">~

</td>

<td>(

</td>

<td>c

</td>

<td>)

</td>

<td style="background-color:#FDE9D9">V

</td>

<td>b

</td>

<td>)

</td>

<td>)

</td></tr>

<td style="background-color:#F2F2F2" height="12">0,1

</td>

<td>0

</td>

<td>0

</td>

<td>1

</td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#DBE5F1">1

</td>

<td>1

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#DDD9C3">1

</td>

<td>

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>0

</td>

<td>

</td>

<td>

</td></tr>

<td style="background-color:#F2F2F2" height="12">2,3

</td>

<td>0

</td>

<td>1

</td>

<td>1

</td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#DBE5F1">1

</td>

<td>1

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#DDD9C3">1

</td>

<td>

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>1

</td>

<td>

</td>

<td>

</td></tr>

<td style="background-color:#F2F2F2" height="12">4,5

</td>

<td>1

</td>

<td>0

</td>

<td>1

</td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>

</td>

<td style="background-color:#EAF1DD">0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>1

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#DDD9C3">1

</td>

<td>

</td>

<td style="background-color:#EAF1DD">0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>0

</td>

<td>

</td>

<td>

</td></tr>

<td style="background-color:#F2F2F2" height="12">6,7

</td>

<td>1

</td>

<td>1

</td>

<td>1

</td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBE5F1">1

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>

</td>

<td style="background-color:#EAF1DD">0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>1

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#DDD9C3">1

</td>

<td>

</td>

<td style="background-color:#EAF1DD">0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>1

</td>

<td>

</td>

<td>

</td></tr></tbody></table>

<div class="mw-heading mw-heading2"><h2 id="Normal_forms">Normal forms</h2></div>

<p>An arbitrary propositional formula may have a very complicated structure. It is often convenient to work with formulas that have simpler forms, known as <b>normal forms</b>. Some common normal forms include <a href="Conjunctive_normal_form" title="Conjunctive normal form">conjunctive normal form</a> and <a href="Disjunctive_normal_form" title="Disjunctive normal form">disjunctive normal form</a>. Any propositional formula can be reduced to its conjunctive or disjunctive normal form.

</p>

<div class="mw-heading mw-heading3"><h3 id="Reduction_to_normal_form">Reduction to normal form</h3></div>

<p>Reduction to normal form is relatively simple once a truth table for the formula is prepared. But further attempts to minimize the number of literals (see below) requires some tools: reduction by De Morgan's laws and <a href="Truth_table" title="Truth table">truth tables</a> can be unwieldy, but <a href="Karnaugh_map" title="Karnaugh map">Karnaugh maps</a> are very suitable a small number of variables (5 or less). Some sophisticated tabular methods exist for more complex circuits with multiple outputs but these are beyond the scope of this article; for more see <a href="Quine%E2%80%93McCluskey_algorithm" title="Quine–McCluskey algorithm">Quine–McCluskey algorithm</a>.

</p>

<div class="mw-heading mw-heading4"><h4 id="Literal,_term_and_alterm">Literal, term and alterm</h4></div>

<p>In electrical engineering, a variable x or its negation ~(x) can be referred to as a <a href="Literal_(mathematical_logic)" title="Literal (mathematical logic)">literal</a>. A string of literals connected by ANDs is called a term. A string of literals connected by OR is called an alterm. Typically the literal ~(x) is abbreviated ~x. Sometimes the &-symbol is omitted altogether in the manner of algebraic multiplication.

</p>

<ul><li>Examples

<ol><li>a, b, c, d are variables. ((( a & ~(b) ) & ~(c)) & d) is a term. This can be abbreviated as (a & ~b & ~c & d), or a~b~cd.</li>

<li>p, q, r, s are variables. (((p ∨ ~(q) ) ∨ r) ∨ ~(s) ) is an alterm. This can be abbreviated as (p ∨ ~q ∨ r ∨ ~s).</li></ol></li></ul>

<div class="mw-heading mw-heading4"><h4 id="Minterms">Minterms</h4></div>

<p>In the same way that a 2<sup>n</sup>-row truth table displays the evaluation of a propositional formula for all 2<sup>n</sup> possible values of its variables, n variables produces a 2<sup>n</sup>-square Karnaugh map (even though we cannot draw it in its full-dimensional realization). For example, 3 variables produces 2<sup>3</sup> = 8 rows and 8 Karnaugh squares; 4 variables produces 16 truth-table rows and 16 squares and therefore 16 <a href="Minterms" class="mw-redirect" title="Minterms">minterms</a>. Each Karnaugh-map square and its corresponding truth-table evaluation represents one minterm.

</p><p>Any propositional formula can be reduced to the "logical sum" (OR) of the active (i.e. "1"- or "T"-valued) minterms. When in this form the formula is said to be in <a href="Disjunctive_normal_form" title="Disjunctive normal form">disjunctive normal form</a>. But even though it is in this form, it is not necessarily minimized with respect to either the number of terms or the number of literals.

</p><p>In the following table, observe the peculiar numbering of the rows: (0, 1, 3, 2, 6, 7, 5, 4, 0). The first column is the decimal equivalent of the binary equivalent of the digits "cba", in other words:

</p>

<ul><li>Example

<p>This numbering comes about because as one moves down the table from row to row only one variable at a time changes its value. <a href="Gray_code" title="Gray code">Gray code</a> is derived from this notion. This notion can be extended to three and four-dimensional <a href="Hypercube" title="Hypercube">hypercubes</a> called <a href="Hasse_diagram" title="Hasse diagram">Hasse diagrams</a> where each corner's variables change only one at a time as one moves around the edges of the cube. Hasse diagrams (hypercubes) flattened into two dimensions are either <a href="Veitch_diagram" class="mw-redirect" title="Veitch diagram">Veitch diagrams</a> or <a href="Karnaugh_map" title="Karnaugh map">Karnaugh maps</a> (these are virtually the same thing).

</p><p>When working with Karnaugh maps one must always keep in mind that the top edge "wrap arounds" to the bottom edge, and the left edge wraps around to the right edge—the Karnaugh diagram is really a three- or four- or n-dimensional flattened object.

</p>

<th width="60" height="39">decimal equivalent of (c, b, a)

</th>

<th>c

</th>

<th>b

</th>

<th>a

</th>

<th>minterm

</th></tr>

<td height="15">0

</td>

<td>0

</td>

<td>0

</td>

<td>0

</td>

<td style="background-color:#FDE9D9">(~c & ~b & ~a)

</td></tr>

<td height="15">1

</td>

<td>0

</td>

<td>0

</td>

<td>1

</td>

<td style="background-color:#FDE9D9">(~c & ~b & a)

</td></tr>

<td height="12">3

</td>

<td>0

</td>

<td>1

</td>

<td>1

</td>

<td style="background-color:#FDE9D9">(~c & b & a)

</td></tr>

<td height="12">2

</td>

<td>0

</td>

<td>1

</td>

<td>0

</td>

<td style="background-color:#FDE9D9">(~c & b & ~a)

</td></tr>

<td height="12">6

</td>

<td>1

</td>

<td>1

</td>

<td>0

</td>

<td style="background-color:#FDE9D9">(c & b & ~a)

</td></tr>

<td height="12">7

</td>

<td>1

</td>

<td>1

</td>

<td>1

</td>

<td style="background-color:#FDE9D9">(c & b & a)

</td></tr>

<td height="12">5

</td>

<td>1

</td>

<td>0

</td>

<td>1

</td>

<td style="background-color:#FDE9D9">(c & ~b & a)

</td></tr>

<td height="12">4

</td>

<td>1

</td>

<td>0

</td>

<td>0

</td>

<td style="background-color:#FDE9D9">(c & ~b & ~a)

</td></tr>

<td height="12">0

</td>

<td style="font-weight:bold">0

</td>

<td>0

</td>

<td>0

</td>

<td>(~a & ~b & ~c)

</td></tr></tbody></table>

<div class="mw-heading mw-heading3"><h3 id="Reduction_by_use_of_the_map_method_(Veitch,_Karnaugh)">Reduction by use of the map method (Veitch, Karnaugh)</h3></div>

<p>Veitch improved the notion of <a href="Venn_diagram" title="Venn diagram">Venn diagrams</a> by converting the circles to abutting squares, and Karnaugh simplified the Veitch diagram by converting the minterms, written in their literal-form (e.g. ~abc~d) into numbers.<sup id="cite_ref-24" class="reference"><a href="#cite_note-24"><span class="cite-bracket">[</span>22<span class="cite-bracket">]</span></a></sup> The method proceeds as follows:

</p>

<div class="mw-heading mw-heading4"><h4 id="Produce_the_formula's_truth_table">Produce the formula's truth table</h4></div>

<p>Produce the formula's truth table. Number its rows using the binary-equivalents of the variables (usually just sequentially 0 through n-1) for n variables.

</p>

<dl><dd><i>Technically, the <a href="Propositional_function" title="Propositional function">propositional function</a> has been reduced to its (unminimized) conjunctive normal form: each row has its minterm expression and these can be OR'd to produce the formula in its (unminimized) conjunctive normal form.</i></dd></dl>

<p>Example: ((c & d) ∨ (p & ~(c & (~d)))) = q in conjunctive normal form is:

</p>

<p>However, this formula be reduced both in the number of terms (from 4 to 3) and in the total count of its literals (12 to 6).

</p>

<table>

<th style="background-color:#F2F2F2" width="25.5" height="24">row

</th>

<th>Minterms

</th>

<th width="21">p

</th>

<th width="21">d

</th>

<th width="21">c

</th>

<th width="10.5">(

</th>

<th width="10.5">(

</th>

<th width="10.5">c

</th>

<th width="10.5">&

</th>

<th width="10.5">d

</th>

<th width="10.5">)

</th>

<th style="background-color:#FDE9D9" width="10.5">∨

</th>

<th width="10.5">(

</th>

<th width="10.5">p

</th>

<th width="10.5">&

</th>

<th width="10.5">~

</th>

<th width="10.5">(

</th>

<th width="10.5">(

</th>

<th width="10.5">c

</th>

<th width="10.5">&

</th>

<th width="10.5">~

</th>

<th width="10.5">(

</th>

<th width="10.5">d

</th>

<th width="10.5">)

</th>

<th width="10.5">)

</th>

<th width="10.5">)

</th>

<th width="10.5">)

</th>

<th width="10.5">)

</th>

<th style="background: #9EFF9E; color:black; vertical-align: middle; text-align: center;" class="active table-active">Active minterms

</th>

<th>Formula in conjunctive normal form

</th></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12" align="center" valign="bottom">0

</td>

<td align="center" valign="bottom">( ~p & ~d & ~c )

</td>

<td align="center" valign="bottom">0

</td>

<td align="center" valign="bottom">0

</td>

<td align="center" valign="bottom">0

</td>

</td>

</td>

<td align="center" valign="bottom">0

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">0

</td>

<td align="center" valign="bottom">0

</td>

</td>

<td style="background-color:#FDE9D9" align="center" valign="bottom">0

</td>

</td>

<td align="center" valign="bottom">0

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">0

</td>

<td style="background-color:#EAF1DD" align="center" valign="bottom">1

</td>

</td>

</td>

<td align="center" valign="bottom">0

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">0

</td>

<td style="background-color:#EAF1DD" align="center" valign="bottom">1

</td>

</td>

<td align="center" valign="bottom">0

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12" align="center" valign="bottom">1

</td>

<td align="center" valign="bottom">( ~p & ~d & c)

</td>

<td align="center" valign="bottom">0

</td>

<td align="center" valign="bottom">0

</td>

<td align="center" valign="bottom">1

</td>

</td>

</td>

<td align="center" valign="bottom">1

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">0

</td>

<td align="center" valign="bottom">0

</td>

</td>

<td style="background-color:#FDE9D9" align="center" valign="bottom">0

</td>

</td>

<td align="center" valign="bottom">0

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">0

</td>

<td style="background-color:#EAF1DD" align="center" valign="bottom">0

</td>

</td>

</td>

<td align="center" valign="bottom">1

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">1

</td>

<td style="background-color:#EAF1DD" align="center" valign="bottom">1

</td>

</td>

<td align="center" valign="bottom">0

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12" align="center" valign="bottom">2

</td>

<td align="center" valign="bottom">( ~p & d & ~c )

</td>

<td align="center" valign="bottom">0

</td>

<td align="center" valign="bottom">1

</td>

<td align="center" valign="bottom">0

</td>

</td>

</td>

<td align="center" valign="bottom">0

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">0

</td>

<td align="center" valign="bottom">1

</td>

</td>

<td style="background-color:#FDE9D9" align="center" valign="bottom">0

</td>

</td>

<td align="center" valign="bottom">0

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">0

</td>

<td style="background-color:#EAF1DD" align="center" valign="bottom">1

</td>

</td>

</td>

<td align="center" valign="bottom">0

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">0

</td>

<td style="background-color:#EAF1DD" align="center" valign="bottom">0

</td>

</td>

<td align="center" valign="bottom">1

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12" align="center" valign="bottom">3

</td>

<td align="center" valign="bottom">( ~p & d & c )

</td>

<td align="center" valign="bottom">0

</td>

<td align="center" valign="bottom">1

</td>

<td align="center" valign="bottom">1

</td>

</td>

</td>

<td align="center" valign="bottom">1

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">1

</td>

<td align="center" valign="bottom">1

</td>

</td>

<td style="background-color:#FCD5B4" align="center" valign="bottom">1

</td>

</td>

<td align="center" valign="bottom">0

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">0

</td>

<td style="background-color:#EAF1DD" align="center" valign="bottom">1

</td>

</td>

</td>

<td align="center" valign="bottom">1

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">0

</td>

<td style="background-color:#EAF1DD" align="center" valign="bottom">0

</td>

</td>

<td align="center" valign="bottom">1

</td>

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#FCD5B4" align="center">(~p & d & c)

</td>

</td></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12" align="center" valign="bottom">4

</td>

<td align="center" valign="bottom">( p & ~d & ~c )

</td>

<td align="center" valign="bottom">1

</td>

<td align="center" valign="bottom">0

</td>

<td align="center" valign="bottom">0

</td>

</td>

</td>

<td align="center" valign="bottom">0

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">0

</td>

<td align="center" valign="bottom">0

</td>

</td>

<td style="background-color:#FCD5B4" align="center" valign="bottom">1

</td>

</td>

<td align="center" valign="bottom">1

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">1

</td>

<td style="background-color:#EAF1DD" align="center" valign="bottom">1

</td>

</td>

</td>

<td align="center" valign="bottom">0

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">0

</td>

<td style="background-color:#EAF1DD" align="center" valign="bottom">1

</td>

</td>

<td align="center" valign="bottom">0

</td>

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#FCD5B4" align="center">(~p & d & c)

</td>

</td></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12" align="center" valign="bottom">5

</td>

<td align="center" valign="bottom">( p & ~d & c )

</td>

<td align="center" valign="bottom">1

</td>

<td align="center" valign="bottom">0

</td>

<td align="center" valign="bottom">1

</td>

</td>

</td>

<td align="center" valign="bottom">1

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">0

</td>

<td align="center" valign="bottom">0

</td>

</td>

<td style="background-color:#FDE9D9" align="center" valign="bottom">0

</td>

</td>

<td align="center" valign="bottom">1

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">0

</td>

<td style="background-color:#EAF1DD" align="center" valign="bottom">0

</td>

</td>

</td>

<td align="center" valign="bottom">1

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">1

</td>

<td style="background-color:#EAF1DD" align="center" valign="bottom">1

</td>

</td>

<td align="center" valign="bottom">0

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12" align="center" valign="bottom">6

</td>

<td align="center" valign="bottom">( p & d & ~c )

</td>

<td align="center" valign="bottom">1

</td>

<td align="center" valign="bottom">1

</td>

<td align="center" valign="bottom">0

</td>

</td>

</td>

<td align="center" valign="bottom">0

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">0

</td>

<td align="center" valign="bottom">1

</td>

</td>

<td style="background-color:#FCD5B4" align="center" valign="bottom">1

</td>

</td>

<td align="center" valign="bottom">1

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">1

</td>

<td style="background-color:#EAF1DD" align="center" valign="bottom">1

</td>

</td>

</td>

<td align="center" valign="bottom">0

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">0

</td>

<td style="background-color:#EAF1DD" align="center" valign="bottom">0

</td>

</td>

<td align="center" valign="bottom">1

</td>

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#FCD5B4" align="center">(p & d & ~c)

</td>

</td></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12" align="center" valign="bottom">7

</td>

<td align="center" valign="bottom">( p & d & c )

</td>

<td align="center" valign="bottom">1

</td>

<td align="center" valign="bottom">1

</td>

<td align="center" valign="bottom">1

</td>

</td>

</td>

<td align="center" valign="bottom">0

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">1

</td>

<td align="center" valign="bottom">1

</td>

</td>

<td style="background-color:#FCD5B4" align="center" valign="bottom">1

</td>

</td>

<td align="center" valign="bottom">1

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">1

</td>

<td style="background-color:#EAF1DD" align="center" valign="bottom">1

</td>

</td>

</td>

<td align="center" valign="bottom">1

</td>

<td style="background-color:#DBE5F1" align="center" valign="bottom">0

</td>

<td style="background-color:#EAF1DD" align="center" valign="bottom">0

</td>

</td>

<td align="center" valign="bottom">1

</td>

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#FCD5B4" align="center">( p & d & c )

</td>

</td></tr>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#FFA7A9;font-weight:bold" align="center">q

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#FFA7A9" align="center">= (~p&d&c) ∨ (~p&d&c) ∨ (p&d&~c ) ∨ (p&d&c )

</td></tr></tbody></table>

<div class="mw-heading mw-heading4"><h4 id="Create_the_formula's_Karnaugh_map">Create the formula's Karnaugh map</h4></div>

<p>Use the values of the formula (e.g. "p") found by the truth-table method and place them in their into their respective (associated) Karnaugh squares (these are numbered per the Gray code convention). If values of "d" for "don't care" appear in the table, this adds flexibility during the reduction phase.

</p>

<div class="mw-heading mw-heading4"><h4 id="Reduce_minterms">Reduce minterms</h4></div>

<p>Minterms of adjacent (abutting) 1-squares (T-squares) can be reduced with respect to the number of their <a href="Literal_(mathematical_logic)" title="Literal (mathematical logic)">literals</a>, and the number terms also will be reduced in the process. Two abutting squares (2 x 1 horizontal or 1 x 2 vertical, even the edges represent abutting squares) lose one literal, four squares in a 4 x 1 rectangle (horizontal or vertical) or 2 x 2 square (even the four corners represent abutting squares) lose two literals, eight squares in a rectangle lose 3 literals, etc. (One seeks out the largest square or rectangles and ignores the smaller squares or rectangles contained totally within it. ) This process continues until all abutting squares are accounted for, at which point the propositional formula is minimized.

</p><p>For example, squares #3 and #7 abut. These two abutting squares can lose one literal (e.g. "p" from squares #3 and #7), four squares in a rectangle or square lose two literals, eight squares in a rectangle lose 3 literals, etc. (One seeks out the largest square or rectangles.) This process continues until all abutting squares are accounted for, at which point the propositional formula is said to be minimized.

</p><p>Example: The map method usually is done by inspection. The following example expands the algebraic method to show the "trick" behind the combining of terms on a Karnaugh map:

</p>

<dl><dd>Minterms #3 and #7 abut, #7 and #6 abut, and #4 and #6 abut (because the table's edges wrap around). So each of these pairs can be reduced.</dd></dl>

<p>Observe that by the Idempotency law (A ∨ A) = A, we can create more terms. Then by association and distributive laws the variables to disappear can be paired, and then "disappeared" with the Law of contradiction (x & ~x)=0. The following uses brackets [ and ] only to keep track of the terms; they have no special significance:

</p>

<ul><li>Put the formula in conjunctive normal form with the formula to be reduced:</li></ul>

<ul><li>Idempotency (absorption) [ A ∨ A) = A:</li></ul>

<ul><li>Associative law (x ∨ (y ∨ z)) = ( (x ∨ y) ∨ z )</li></ul>

<ul><li>Distributive law ( x & (y ∨ z) ) = ( (x & y) ∨ (x & z) ) :</li></ul>

<ul><li>Commutative law and law of contradiction (x & ~x) = (~x & x) = 0:</li></ul>

<ul><li>Law of identity ( x ∨ 0 ) = x leading to the reduced form of the formula:</li></ul>

<div class="mw-heading mw-heading4"><h4 id="Verify_reduction_with_a_truth_table">Verify reduction with a truth table</h4></div>

<table>

<td style="background-color:#F2F2F2" width="25.5" height="12">row

</td>

<th>Minterms

</th>

<th width="21">p

</th>

<th width="21">d

</th>

<th width="21">c

</th>

<th width="10.5">(

</th>

<th width="10.5">(

</th>

<th width="10.5">d

</th>

<th style="background-color:#DBE5F1" width="10.5">&

</th>

<th width="10.5">c

</th>

<th width="10.5">)

</th>

<th style="background-color:#FDE9D9" width="10.5">∨

</th>

<th width="10.5">(

</th>

<th width="10.5">p

</th>

<th style="background-color:#DBE5F1" width="10.5">&

</th>

<th width="10.5">d

</th>

<th width="10.5">)

</th>

<th style="background-color:#FDE9D9" width="10.5">∨

</th>

<th width="10.5">(

</th>

<th width="10.5">p

</th>

<th style="background-color:#DBE5F1" width="10.5">&

</th>

<th style="background-color:#EAF1DD" width="10.5">~

</th>

<th width="10.5">(

</th>

<th width="10.5">c

</th>

<th width="10.5">)

</th>

<th width="10.5">)

</th></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12">0

</td>

<td>( ~p & ~d & ~c )

</td>

<td>0

</td>

<td>0

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td>

</td></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12">1

</td>

<td>( ~p & ~d & c)

</td>

<td>0

</td>

<td>0

</td>

<td>1

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#EAF1DD">0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>

</td></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12">2

</td>

<td>( ~p & d & ~c )

</td>

<td>0

</td>

<td>1

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td>

</td></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12">3

</td>

<td>( ~p & d & c )

</td>

<td>0

</td>

<td>1

</td>

<td>1

</td>

<td>

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBE5F1">1

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#FAC090">1

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#EAF1DD">0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>

</td></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12">4

</td>

<td>( p & ~d & ~c )

</td>

<td>1

</td>

<td>0

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#FAC090">1

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBE5F1">1

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td>

</td></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12">5

</td>

<td>( p & ~d & c )

</td>

<td>1

</td>

<td>0

</td>

<td>1

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#EAF1DD">0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>

</td></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12">6

</td>

<td>( p & d & ~c )

</td>

<td>1

</td>

<td>1

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBE5F1">1

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#FAC090">1

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBE5F1">1

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td>

</td></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12">7

</td>

<td>( p & d & c )

</td>

<td>1

</td>

<td>1

</td>

<td>1

</td>

<td>

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBE5F1">1

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBE5F1">1

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#FAC090">1

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#EAF1DD">0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>

</td></tr>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#FAC090;font-weight:bold" align="center">q

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td>

</td></tr></tbody></table>

<div class="mw-heading mw-heading2"><h2 id="Impredicative_propositions">Impredicative propositions</h2></div>

<p>Given the following examples-as-definitions, what does one make of the subsequent reasoning:

</p>

<dl><dd>(1) "This sentence is simple." (2) "This sentence is complex, and it is conjoined by AND."</dd></dl>

<p>Then assign the variable "s" to the left-most sentence "This sentence is simple". Define "compound" c = "not simple" ~s, and assign c = ~s to "This sentence is compound"; assign "j" to "It [this sentence] is conjoined by AND". The second sentence can be expressed as:

</p>

<p>If truth values are to be placed on the sentences c = ~s and j, then all are clearly FALSEHOODS: e.g. "This sentence is complex" is a FALSEHOOD (it is <i>simple</i>, by definition). So their conjunction (AND) is a falsehood. But when taken in its assembled form, the sentence a TRUTH.

</p><p>This is an example of the <a href="Paradox" title="Paradox">paradoxes</a> that result from an <a href="Impredicative_definition" class="mw-redirect" title="Impredicative definition">impredicative definition</a>—that is, when an object m has a property P, but the object m is defined in terms of property P.<sup id="cite_ref-25" class="reference"><a href="#cite_note-25"><span class="cite-bracket">[</span>23<span class="cite-bracket">]</span></a></sup> The best advice for a rhetorician or one involved in deductive analysis is avoid impredicative definitions but at the same time be on the lookout for them because they can indeed create paradoxes. Engineers, on the other hand, put them to work in the form of propositional formulas with feedback.

</p>

<div class="mw-heading mw-heading2"><h2 id="Propositional_formula_with_"feedback"">Propositional formula with "feedback"</h2></div>

<p>The notion of a propositional formula appearing as one of its own variables requires a formation rule that allows the assignment of the formula to a variable. In general there is no stipulation (either axiomatic or truth-table systems of objects and relations) that forbids this from happening.<sup id="cite_ref-26" class="reference"><a href="#cite_note-26"><span class="cite-bracket">[</span>24<span class="cite-bracket">]</span></a></sup>

</p><p>The simplest case occurs when an OR formula becomes one its own inputs e.g. p = q. Begin with (p ∨ s) = q, then let p = q. Observe that q's "definition" depends on itself "q" as well as on "s" and the OR connective; this definition of q is thus impredicative.

Either of two conditions can result:<sup id="cite_ref-27" class="reference"><a href="#cite_note-27"><span class="cite-bracket">[</span>25<span class="cite-bracket">]</span></a></sup> oscillation or memory.

</p><p>It helps to think of the formula as a <a href="Black_box" title="Black box">black box</a>. Without knowledge of what is going on "inside" the formula-"box" from the outside it would appear that the output is no longer a <a href="Function_(mathematics)" title="Function (mathematics)">function</a> of the inputs alone. That is, sometimes one looks at q and sees 0 and other times 1. To avoid this problem one has to know the state (condition) of the "hidden" variable p inside the box (i.e. the value of q fed back and assigned to p). When this is known the apparent inconsistency goes away.

</p><p>To understand [predict] the behavior of formulas with feedback requires the more sophisticated analysis of <a href="Sequential_circuit" class="mw-redirect" title="Sequential circuit">sequential circuits</a>. Propositional formulas with feedback lead, in their simplest form, to state machines; they also lead to memories in the form of Turing tapes and counter-machine counters. From combinations of these elements one can build any sort of bounded computational model (e.g. <a href="Turing_machine" title="Turing machine">Turing machines</a>, <a href="Counter_machine" title="Counter machine">counter machines</a>, <a href="Register_machine" title="Register machine">register machines</a>, <a href="Macintosh_computer" class="mw-redirect" title="Macintosh computer">Macintosh computers</a>, etc.).

</p>

<div class="mw-heading mw-heading3"><h3 id="Oscillation">Oscillation</h3></div>

<p>In the abstract (ideal) case the simplest oscillating formula is a NOT fed back to itself: ~(~(p=q)) = q. Analysis of an abstract (ideal) propositional formula in a truth-table reveals an inconsistency for both p=1 and p=0 cases: When p=1, q=0, this cannot be because p=q; ditto for when p=0 and q=1.

</p>

<table>

</th>

</th>

<th style="background-color:#EAF1DD;font-weight:bold" width="14.25">q

</th>

</th>

</th>

</th>

</th>

</th></tr>

<th style="font-weight:bold" height="12">p

</th>

<th>

</th>

<th style="background-color:#EAF1DD;font-weight:bold">~

</th>

<th style="font-weight:bold">(

</th>

<th style="font-weight:bold">p

</th>

<th style="font-weight:bold">)

</th>

<th style="font-weight:bold">= q

</th>

<th>

</th></tr>

<td height="12">0

</td>

<td>

</td>

<td style="background-color:red">1

</td>

</td>

<td style="background-color:red">0

</td>

</td>

<td style="background-color:#D8D8D8">1

</td>

<td style="background-color:#D8D8D8">q & p inconsistent

</td></tr>

<td height="12">1

</td>

<td>

</td>

<td style="background-color:red">0

</td>

</td>

<td style="background-color:red">1

</td>

</td>

<td style="background-color:#D8D8D8">0

</td>

<td style="background-color:#D8D8D8">q & p inconsistent

</td></tr></tbody></table>

<p><b>Oscillation with delay</b>: If a delay<sup id="cite_ref-28" class="reference"><a href="#cite_note-28"><span class="cite-bracket">[</span>26<span class="cite-bracket">]</span></a></sup> (ideal or non-ideal) is inserted in the abstract formula between p and q then p will oscillate between 1 and 0: 101010...101... <i>ad infinitum</i>. If either of the delay and NOT are not abstract (i.e. not ideal), the type of analysis to be used will be dependent upon the exact nature of the objects that make up the oscillator; such things fall outside mathematics and into engineering.

</p><p>Analysis requires a delay to be inserted and then the loop cut between the delay and the input "p". The delay must be viewed as a kind of proposition that has "qd" (q-delayed) as output for "q" as input. This new proposition adds another column to the truth table. The inconsistency is now between "qd" and "p" as shown in red; two stable states resulting:

</p>

<table>

</th>

</th>

</th>

<th style="background-color:#EAF1DD;font-weight:bold" width="14.25">q

</th>

</th>

</th>

</th>

</th>

</th></tr>

<th style="font-weight:bold" height="12">qd

</th>

<th style="font-weight:bold">p

</th>

<th style="font-weight:bold">(

</th>

<th style="background-color:#EAF1DD;font-weight:bold">~

</th>

<th style="font-weight:bold">(

</th>

<th style="font-weight:bold">p

</th>

<th style="font-weight:bold">)

</th>

<th style="background-color:#EAF1DD;font-weight:bold">= q

</th>

<th>

</th></tr>

<td height="12">0

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>state 1

</td></tr>

<td style="background-color:red" height="12">0

</td>

<td style="background-color:red">1

</td>

</td>

<td style="background-color:#D8D8D8">0

</td>

</td>

<td style="background-color:#D8D8D8">1

</td>

</td>

<td style="background-color:#D8D8D8">0

</td>

<td style="background-color:#D8D8D8">qd & p inconsistent

</td></tr>

<td style="background-color:red" height="12">1

</td>

<td style="background-color:red">0

</td>

</td>

<td style="background-color:#D8D8D8">1

</td>

</td>

<td style="background-color:#D8D8D8">0

</td>

</td>

<td style="background-color:#D8D8D8">1

</td>

<td style="background-color:#D8D8D8">qd & p inconsistent

</td></tr>

<td height="12">1

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#EAF1DD">0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#EAF1DD">0

</td>

<td>state 0

</td></tr></tbody></table>

<div class="mw-heading mw-heading3"><h3 id="Memory">Memory</h3></div>

<p>Without delay, inconsistencies must be eliminated from a truth table analysis. With the notion of "delay", this condition presents itself as a momentary inconsistency between the fed-back output variable q and p = q<sub>delayed</sub>.

</p><p>A truth table reveals the rows where inconsistencies occur between p = q<sub>delayed</sub> at the input and q at the output. After "breaking" the feed-back,<sup id="cite_ref-29" class="reference"><a href="#cite_note-29"><span class="cite-bracket">[</span>27<span class="cite-bracket">]</span></a></sup> the truth table construction proceeds in the conventional manner. But afterwards, in every row the output q is compared to the now-independent input p and any inconsistencies between p and q are noted (i.e. p=0 together with q=1, or p=1 and q=0); when the "line" is "remade" both are rendered impossible by the Law of contradiction ~(p & ~p)). Rows revealing inconsistencies are either considered <a href="Transient_state" title="Transient state">transient states</a> or just eliminated as inconsistent and hence "impossible".

</p>

<div class="mw-heading mw-heading4"><h4 id="Once-flip_memory">Once-flip memory</h4></div>

<p>About the simplest memory results when the output of an OR feeds back to one of its inputs, in this case output "q" feeds back into "p". Given that the formula is first evaluated (initialized) with p=0 & q=0, it will "flip" once when "set" by s=1. Thereafter, output "q" will sustain "q" in the "flipped" condition (state q=1). This behavior, now time-dependent, is shown by the <a href="State_diagram" title="State diagram">state diagram</a> to the right of the once-flip.

</p>

<table>

</th>

</th>

</th>

</th>

<th style="background-color:#FDE9D9;font-weight:bold" width="14.25">q

</th>

</th>

</th>

</th>

</th></tr>

<th style="font-weight:bold" height="12">p

</th>

<th style="font-weight:bold">s

</th>

<th style="font-weight:bold">(

</th>

<th style="background-color:#FCFF7F;font-weight:bold">s

</th>

<th style="background-color:#FDE9D9;font-weight:bold">∨

</th>

<th style="font-weight:bold">p

</th>

<th style="font-weight:bold">)

</th>

<th style="background-color:#FDE9D9;font-weight:bold">= q

</th>

<th>

</th></tr>

<td height="12">0

</td>

<td>0

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>state 0, s=0

</td></tr>

<td style="background-color:#BFBFBF" height="12">0

</td>

<td style="background-color:#BFBFBF">1

</td>

</td>

<td style="background-color:#BFBFBF">1

</td>

<td style="background-color:red">1

</td>

<td style="background-color:red">0

</td>

</td>

</td>

<td style="background-color:#D8D8D8">q & p inconsistent

</td></tr>

<td height="12">1

</td>

<td>0

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>state 1 with s = 0

</td></tr>

<td height="12">1

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#FCFF7F">1

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>state 1 with s = 1

</td></tr></tbody></table>

<div class="mw-heading mw-heading4"><h4 id="Flip-flop_memory">Flip-flop memory</h4></div>

<p>The next simplest case is the "set-reset" <a href="Flip-flop_(electronics)" title="Flip-flop (electronics)">flip-flop</a> shown below the once-flip. Given that r=0 & s=0 and q=0 at the outset, it is "set" (s=1) in a manner similar to the once-flip. It however has a provision to "reset" q=0 when "r"=1. And additional complication occurs if both set=1 and reset=1. In this formula, the set=1 <i>forces</i> the output q=1 so when and if (s=0 & r=1) the flip-flop will be reset. Or, if (s=1 & r=0) the flip-flop will be set. In the abstract (ideal) instance in which s=1 ⇒ s=0 & r=1 ⇒ r=0 simultaneously, the formula q will be indeterminate (undecidable). Due to delays in "real" OR, AND and NOT the result will be unknown at the outset but thereafter predicable.

</p>

<table>

</th>

</th>

</th>

</th>

</th>

<th style="background-color:#FDE9D9;font-weight:bold" width="14.25">q

</th>

</th>

</th>

</th>

</th>

</th>

</th>

</th>

</th>

</th>

</th>

</th></tr>

<th style="font-weight:bold" height="12">p

</th>

<th style="font-weight:bold">s

</th>

<th style="font-weight:bold">r

</th>

<th style="font-weight:bold">(

</th>

<th style="background-color:#FCFF7F;font-weight:bold">s

</th>

<th style="background-color:#FDE9D9;font-weight:bold">∨

</th>

<th style="font-weight:bold">(

</th>

<th style="font-weight:bold">p

</th>

<th style="background-color:#DBE5F1;font-weight:bold">&

</th>

<th style="background-color:#EAF1DD;font-weight:bold">~

</th>

<th style="font-weight:bold">(

</th>

<th style="background-color:#FCFF7F;font-weight:bold">r

</th>

<th style="font-weight:bold">)

</th>

<th style="font-weight:bold">)

</th>

<th style="font-weight:bold">)

</th>

<th style="background-color:#FDE9D9;font-weight:bold">= q

</th>

<th>

</th></tr>

<td height="12">0

</td>

<td>0

</td>

<td>0

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>state 0 with ( s=0 & r=0 )

</td></tr>

<td height="12">0

</td>

<td>0

</td>

<td>1

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#EAF1DD">0

</td>

<td>

</td>

<td style="background-color:#FCFF7F">1

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>state 0 with ( s=0 & r=1 )

</td></tr>

<td style="background-color:#D8D8D8" height="12">0

</td>

<td style="background-color:#D8D8D8">1

</td>

<td style="background-color:#D8D8D8">0

</td>

</td>

<td style="background-color:#D8D8D8">1

</td>

<td style="background-color:red">1

</td>

</td>

<td style="background-color:red">0

</td>

<td style="background-color:#D8D8D8">0

</td>

<td style="background-color:#D8D8D8">1

</td>

</td>

<td style="background-color:#D8D8D8">0

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#D8D8D8">q & p inconsistent

</td></tr>

<td style="background-color:#D8D8D8" height="12">0

</td>

<td style="background-color:#D8D8D8">1

</td>

<td style="background-color:#D8D8D8">1

</td>

</td>

<td style="background-color:#D8D8D8">1

</td>

<td style="background-color:red">1

</td>

</td>

<td style="background-color:red">0

</td>

<td style="background-color:#D8D8D8">0

</td>

<td style="background-color:#D8D8D8">0

</td>

</td>

<td style="background-color:#D8D8D8">1

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#D8D8D8">q & p inconsistent

</td></tr>

<td height="12">1

</td>

<td>0

</td>

<td>0

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBE5F1">1

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>state 1 with ( s=0 & r=0 )

</td></tr>

<td style="background-color:#D8D8D8" height="12">1

</td>

<td style="background-color:#D8D8D8">0

</td>

<td style="background-color:#D8D8D8">1

</td>

</td>

<td style="background-color:#D8D8D8">0

</td>

<td style="background-color:red">0

</td>

</td>

<td style="background-color:red">1

</td>

<td style="background-color:#D8D8D8">0

</td>

<td style="background-color:#D8D8D8">0

</td>

</td>

<td style="background-color:#D8D8D8">1

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#D8D8D8">q & p inconsistent

</td></tr>

<td height="12">1

</td>

<td>1

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#FCFF7F">1

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>

</td>

<td>1

</td>

<td style="background-color:#DBE5F1">1

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>state 1 with ( s=1 & r=0 )

</td></tr>

<td style="background-color:#F2F2F2" height="12">1

</td>

<td style="background-color:#F2F2F2">1

</td>

<td style="background-color:#F2F2F2">1

</td>

</td>

<td style="background-color:#FCFF7F">1

</td>

<td style="background-color:#FDE9D9">1

</td>

</td>

<td style="background-color:#F2F2F2">1

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#EAF1DD">0

</td>

</td>

<td style="background-color:#FCFF7F">1

</td>

</td>

</td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td style="background-color:#F2F2F2">state 1 with s & r simultaneously 1

</td></tr></tbody></table>

<div class="mw-heading mw-heading4"><h4 id="Clocked_flip-flop_memory">Clocked flip-flop memory</h4></div>

<p>The formula known as "clocked flip-flop" memory ("c" is the "clock" and "d" is the "data") is given below. It works as follows: When c = 0 the data d (either 0 or 1) cannot "get through" to affect output q. When c = 1 the data d "gets through" and output q "follows" d's value. When c goes from 1 to 0 the last value of the data remains "trapped" at output "q". As long as c=0, d can change value without causing q to change.

</p>

<ul><li>Examples

<p>The state diagram is similar in shape to the flip-flop's state diagram, but with different labelling on the transitions.

</p>

<table>

</th>

</th>

</th>

</th>

</th>

</th>

</th>

<th style="background-color:#DBE5F1" width="10.5" align="center">s

</th>

</th>

</th>

<th style="background-color:#FDE9D9;font-weight:bold" width="10.5" align="center">q

</th>

</th>

</th>

<th style="background-color:#DBE5F1" width="10.5" align="center">w

</th>

<th style="background-color:#EAF1DD" width="10.5" align="center">v

</th>

</th>

</th>

</th>

<th style="background-color:#DBE5F1" width="10.5" align="center">r

</th>

<th style="background-color:#EAF1DD" width="10.5" align="center">u

</th>

</th>

</th>

</th>

</th>

</th>

</th>

</th>

</th>

</th></tr>

<th style="background-color:#F2F2F2" height="14.25">row

</th>

<th style="font-weight:bold">q

</th>

<th style="font-weight:bold">d

</th>

<th style="font-weight:bold">c

</th>

<th style="font-weight:bold">(

</th>

<th style="font-weight:bold">(

</th>

<th style="font-weight:bold">c

</th>

<th style="background-color:#DBE5F1;font-weight:bold">&

</th>

<th style="font-weight:bold">d

</th>

<th style="font-weight:bold">)

</th>

<th style="background-color:#FDE9D9;font-weight:bold">∨

</th>

<th style="font-weight:bold">(

</th>

<th style="background-color:#FDE9D9;font-weight:bold">q

</th>

<th style="background-color:#DBE5F1;font-weight:bold">&

</th>

<th style="background-color:#EAF1DD;font-weight:bold">~

</th>

<th style="font-weight:bold">(

</th>

<th style="font-weight:bold">(

</th>

<th style="font-weight:bold">c

</th>

<th style="background-color:#DBE5F1;font-weight:bold">&

</th>

<th style="background-color:#EAF1DD;font-weight:bold">~

</th>

<th style="font-weight:bold">(

</th>

<th style="font-weight:bold">d

</th>

<th style="font-weight:bold">)

</th>

<th style="font-weight:bold">)

</th>

<th style="font-weight:bold">)

</th>

<th style="font-weight:bold">)

</th>

<th style="font-weight:bold">)

</th>

<th style="background-color:#FDE9D9;font-weight:bold">=q

</th>

<th style="font-weight:bold">Description

</th></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12">0

</td>

<td>0

</td>

<td>0

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>state 0 with ( s=0 & r=0 ), 0 is trapped

</td></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12">1

</td>

<td>0

</td>

<td>0

</td>

<td>1

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#FCFF7F">1

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#EAF1DD">0

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#FCFF7F">1

</td>

<td style="background-color:#DBE5F1">1

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>state 0 with ( d=0 & c=1 ):<br>q=0 is following d=0

</td></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12">2

</td>

<td>0

</td>

<td>1

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#EAF1DD">0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#FDE9D9">0

</td>

<td>state 0 with ( d=1 & r=0 ), 0 is trapped

</td></tr>

<td style="background-color:#BFBFBF;font-weight:bold" height="12">3

</td>

<td style="background-color:#BFBFBF">0

</td>

<td style="background-color:#BFBFBF">1

</td>

<td style="background-color:#BFBFBF">1

</td>

</td>

</td>

<td style="background-color:#BFBFBF">1

</td>

<td style="background-color:#BFBFBF">1

</td>

<td style="background-color:#BFBFBF">1

</td>

</td>

<td style="background-color:red">1

</td>

</td>

<td style="background-color:red">0

</td>

<td style="background-color:#BFBFBF">0

</td>

<td style="background-color:#BFBFBF">1

</td>

</td>

</td>

<td style="background-color:#BFBFBF">1

</td>

<td style="background-color:#BFBFBF">0

</td>

<td style="background-color:#BFBFBF">0

</td>

</td>

<td style="background-color:#BFBFBF">1

</td>

</td>

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#D8D8D8">q & p inconsistent

</td></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12">4

</td>

<td>1

</td>

<td>0

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>0

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td style="background-color:#DBE5F1">1

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>state 1 with (d =0 & c=0 ), 1 is trapped

</td></tr>

<td style="background-color:#BFBFBF;font-weight:bold" height="12">5

</td>

<td style="background-color:#BFBFBF">1

</td>

<td style="background-color:#BFBFBF">0

</td>

<td style="background-color:#BFBFBF">1

</td>

</td>

</td>

<td style="background-color:#BFBFBF">1

</td>

<td style="background-color:#BFBFBF">0

</td>

<td style="background-color:#BFBFBF">0

</td>

</td>

<td style="background-color:red">0

</td>

</td>

<td style="background-color:red">1

</td>

<td style="background-color:#BFBFBF">0

</td>

<td style="background-color:#BFBFBF">0

</td>

</td>

</td>

<td style="background-color:#BFBFBF">1

</td>

<td style="background-color:#BFBFBF">1

</td>

<td style="background-color:#BFBFBF">1

</td>

</td>

<td style="background-color:#BFBFBF">0

</td>

</td>

</td>

</td>

</td>

</td>

</td>

<td style="background-color:#D8D8D8">q & p inconsistent

</td></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12">6

</td>

<td>1

</td>

<td>1

</td>

<td>0

</td>

<td>

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td>1

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td style="background-color:#DBE5F1">1

</td>

<td style="background-color:#EAF1DD">1

</td>

</td>

<td>

</td>

<td>0

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#EAF1DD">0

</td>

<td>

</td>

<td>1

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>state 1 with (d =1 & c=0 ), 1 is trapped

</td></tr>

<td style="background-color:#F2F2F2;font-weight:bold" height="12">7

</td>

<td>1

</td>

<td>1

</td>

<td>1

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#FCFF7F">1

</td>

<td style="background-color:#DBE5F1">1

</td>

<td style="background-color:#FCFF7F">1

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td style="background-color:#DBE5F1">1

</td>

<td style="background-color:#EAF1DD">1

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#FCFF7F">1

</td>

<td style="background-color:#DBE5F1">0

</td>

<td style="background-color:#EAF1DD">0

</td>

<td>

</td>

<td style="background-color:#FCFF7F">1

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td>

</td>

<td style="background-color:#FDE9D9">1

</td>

<td>state 1 with ( d=1 & c=1 ):<br>q=1 is following d=1

</td></tr></tbody></table>

<div class="mw-heading mw-heading2"><h2 id="Historical_development">Historical development</h2></div>

<p><a href="Bertrand_Russell" title="Bertrand Russell">Bertrand Russell</a> (1912:74) lists three laws of thought that derive from <a href="Aristotle" title="Aristotle">Aristotle</a>: (1) The <a href="Law_of_identity" title="Law of identity">law of identity</a>: "Whatever is, is.", (2) The <a href="Law_of_noncontradiction" title="Law of noncontradiction">law of noncontradiction</a>: "Nothing can both be and not be", and (3) The <a href="Law_of_excluded_middle" title="Law of excluded middle">law of excluded middle</a>: "Everything must be or not be."

</p>

<ul><li>Example: Here O is an expression about an object's BEING or QUALITY:

<ol><li>Law of Identity: O = O</li>

<li>Law of contradiction: ~(O & ~(O))</li>

<li>Law of excluded middle: (O ∨ ~(O))</li></ol></li></ul>

<p>The use of the word "everything" in the law of excluded middle renders Russell's expression of this law open to debate. If restricted to an expression about BEING or QUALITY with reference to a finite collection of objects (a finite "universe of discourse") -- the members of which can be investigated one after another for the presence or absence of the assertion—then the law is considered intuitionistically appropriate. Thus an assertion such as: "This object must either BE or NOT BE (in the collection)", or "This object must either have this QUALITY or NOT have this QUALITY (relative to the objects in the collection)" is acceptable. See more at <a href="Venn_diagram" title="Venn diagram">Venn diagram</a>.

</p><p>Although a propositional calculus originated with Aristotle, the notion of an <i>algebra</i> applied to propositions had to wait until the early 19th century. In an (adverse) reaction to the 2000 year tradition of Aristotle's <a href="Syllogism" title="Syllogism">syllogisms</a>, <a href="John_Locke" title="John Locke">John Locke</a>'s <i>Essay concerning human understanding (1690)</i> used the word <a href="Semiotics" title="Semiotics">semiotics</a> (theory of the use of symbols). By 1826 <a href="Richard_Whately" title="Richard Whately">Richard Whately</a> had critically analyzed the syllogistic logic with a sympathy toward Locke's semiotics. <a href="George_Bentham" title="George Bentham">George Bentham</a>'s work (1827) resulted in the notion of "quantification of the predicate" (1827) (nowadays symbolized as ∀ ≡ "for all"). A "row" instigated by <a href="Sir_William_Hamilton%2C_9th_Baronet" title="Sir William Hamilton, 9th Baronet">William Hamilton</a> over a priority dispute with <a href="Augustus_De_Morgan" title="Augustus De Morgan">Augustus De Morgan</a> "inspired <a href="George_Boole" title="George Boole">George Boole</a> to write up his ideas on logic, and to publish them as MAL [Mathematical Analysis of Logic] in 1847" (Grattin-Guinness and Bornet 1997:xxviii).

</p><p>About his contribution Grattin-Guinness and Bornet comment:

</p>

<dl><dd>"Boole's principal single innovation was [the] law [ x<sup>n</sup> = x ] for logic: it stated that the mental acts of choosing the property x and choosing x again and again is the same as choosing x once... As consequence of it he formed the equations x•(1-x)=0 and x+(1-x)=1 which for him expressed respectively the law of contradiction and the law of excluded middle" (p. xxviiff). For Boole "1" was the <a href="Universe_of_discourse" class="mw-redirect" title="Universe of discourse">universe of discourse</a> and "0" was nothing.</dd></dl>

<p><a href="Gottlob_Frege" title="Gottlob Frege">Gottlob Frege</a>'s massive undertaking (1879) resulted in a formal calculus of propositions, but his symbolism is so daunting that it had little influence excepting on one person: <a href="Bertrand_Russell" title="Bertrand Russell">Bertrand Russell</a>. First as the student of <a href="Alfred_North_Whitehead" title="Alfred North Whitehead">Alfred North Whitehead</a> he studied Frege's work and suggested a (famous and notorious) emendation with respect to it (1904) around the problem of an <a href="Antinomy" title="Antinomy">antinomy</a> that he discovered in Frege's treatment ( cf <a href="Russell's_paradox" title="Russell's paradox">Russell's paradox</a> ). Russell's work led to a collaboration with Whitehead that, in the year 1912, produced the first volume of <i>Principia Mathematica</i> (PM). It is here that what we consider "modern" propositional logic first appeared. In particular, PM introduces NOT and OR and the assertion symbol ⊦ as primitives. In terms of these notions they define IMPLICATION → ( def. *1.01: ~p ∨ q ), then AND (def. *3.01: ~(~p ∨ ~q) ), then EQUIVALENCE p ←→ q (*4.01: (p → q) & ( q → p ) ).

</p>

<ul><li><a href="Henry_M._Sheffer" title="Henry M. Sheffer">Henry M. Sheffer</a> (1921) and <a href="Jean_Nicod" title="Jean Nicod">Jean Nicod</a> demonstrate that only one connective, the "stroke" | is sufficient to express all propositional formulas.</li>

<li><a href="Emil_Post" class="mw-redirect" title="Emil Post">Emil Post</a> (1921) develops the truth-table method of analysis in his "Introduction to a general theory of elementary propositions". He notes Nicod's stroke | .</li>

<li>Whitehead and Russell add an introduction to their 1927 re-publication of PM adding, in part, a favorable treatment of the "stroke".</li></ul>

<p><b>Computation and switching logic</b>:

</p>

<ul><li><a href="William_Eccles_(physicist)" title="William Eccles (physicist)">William Eccles</a> and <a href="F._W._Jordan" title="F. W. Jordan">F. W. Jordan</a> (1919) describe a "trigger relay" made from a vacuum tube.</li>

<li><a href="George_Stibitz" title="George Stibitz">George Stibitz</a> (1937) invents the binary adder using mechanical relays. He builds this on his kitchen table.</li></ul>

<dl><dd>Example: Given binary <a href="Bit" title="Bit">bits</a> a<sub>i</sub> and b<sub>i</sub> and carry-in ( c_in<sub>i</sub>), their summation Σ<sub>i</sub> and carry-out (c_out<sub>i</sub>) are:

<ul><li><a href="Alan_Turing" title="Alan Turing">Alan Turing</a> builds a multiplier using relays (1937–1938). He has to hand-wind his own relay coils to do this.</li>

<li>Textbooks about "switching circuits" appear in the early 1950s.</li>

<li><a href="Willard_Quine" class="mw-redirect" title="Willard Quine">Willard Quine</a> 1952 and 1955, <a href="Edward_W._Veitch" title="Edward W. Veitch">E. W. Veitch</a> 1952, and <a href="Maurice_Karnaugh" title="Maurice Karnaugh">M. Karnaugh</a> (1953) develop map-methods for simplifying propositional functions.</li>

<li><a href="George_H._Mealy" title="George H. Mealy">George H. Mealy</a> (1955) and <a href="Edward_F._Moore" title="Edward F. Moore">Edward F. Moore</a> (1956) address the theory of sequential (i.e. switching-circuit) "machines".</li>

<li>E. J. McCluskey and H. Shorr develop a method for simplifying propositional (switching) circuits (1962).</li></ul>

<div class="mw-heading mw-heading2"><h2 id="Footnotes">Footnotes</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist reflist-lower-alpha">

<li id="cite_note-13"><span class="mw-cite-backlink"><b><a href="#cite_ref-13">^</a></b></span> <span class="reference-text">Rosenbloom discusses this problem of implication at some length. Most philosophers and mathematicians just accept the material definition as given above. But some do not, including the <a href="Intuitionism" title="Intuitionism">intuitionists</a>; they consider it a form of the law of excluded middle misapplied.<sup id="cite_ref-FOOTNOTERosenbloom195030_and_54ff_12-0" class="reference"><a href="#cite_note-FOOTNOTERosenbloom195030_and_54ff-12"><span class="cite-bracket">[</span>12<span class="cite-bracket">]</span></a></sup></span>

</li>

<li id="cite_note-19"><span class="mw-cite-backlink"><b><a href="#cite_ref-19">^</a></b></span> <span class="reference-text">Rosenbloom<sup id="cite_ref-FOOTNOTERosenbloom195032_18-0" class="reference"><a href="#cite_note-FOOTNOTERosenbloom195032-18"><span class="cite-bracket">[</span>17<span class="cite-bracket">]</span></a></sup> and Kleene 1952:73-74 ranks all 11 symbols.</span>

</li>

</ol></div></div>

<div class="mw-heading mw-heading2"><h2 id="Citations">Citations</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFKaoGenesereth2017" class="citation book cs1">Kao, Eric J.; Genesereth, Michael (2017). <a rel="nofollow" class="external text" href="http://intrologic.stanford.edu/chapters/chapter_02.html">"Propositional Logic"</a>. <i>Introduction to Logic</i>. Synthesis Lectures on Computer Science (3rd ed.). <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-031-01801-5">10.1007/978-3-031-01801-5</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>9783031018015</bdi>.</cite></span>

</li>

<li id="cite_note-2"><span class="mw-cite-backlink"><b><a href="#cite_ref-2">^</a></b></span> <span class="reference-text">Hamilton 1978:1</span>

</li>

<li id="cite_note-3"><span class="mw-cite-backlink"><b><a href="#cite_ref-3">^</a></b></span> <span class="reference-text"><a href="Principia_Mathematica" title="Principia Mathematica">Principia Mathematica</a> (PM) p. 91 eschews "the" because they require a clear-cut "object of sensation"; they stipulate the use of "this"</span>

</li>

<li id="cite_note-4"><span class="mw-cite-backlink"><b><a href="#cite_ref-4">^</a></b></span> <span class="reference-text">(italics added) Reichenbach p.80.</span>

</li>

<li id="cite_note-5"><span class="mw-cite-backlink"><b><a href="#cite_ref-5">^</a></b></span> <span class="reference-text">Tarski p.54-68. Suppes calls IDENTITY a "further rule of inference" and has a brief development around it; Robbin, Bender and Williamson, and Goodstein introduce the sign and its usage without comment or explanation. Hamilton p. 37 employs two signs ≠ and = with respect to the <b>valuation</b> of a formula in a formal calculus. Kleene p. 70 and Hamilton p. 52 place it in the predicate calculus, in particular with regards to the arithmetic of natural numbers.</span>

</li>

<li id="cite_note-6"><span class="mw-cite-backlink"><b><a href="#cite_ref-6">^</a></b></span> <span class="reference-text">Empiricits eschew the notion of <i>a priori</i> (built-in, born-with) knowledge. "Radical reductionists" such as <a href="John_Locke" title="John Locke">John Locke</a> and <a href="David_Hume" title="David Hume">David Hume</a> "held that every idea must either originate directly in sense experience or else be compounded of ideas thus originating"; quoted from Quine reprinted in 1996 <i>The Emergence of Logical Empriricism</i>, Garland Publishing Inc. <a rel="nofollow" class="external free" href="https://www.marxists.org/reference/subject/philosophy/works/us/quine.htm">http://www.marxists.org/reference/subject/philosophy/works/us/quine.htm</a></span>

</li>

<li id="cite_note-7"><span class="mw-cite-backlink"><b><a href="#cite_ref-7">^</a></b></span> <span class="reference-text"><a href="Neural_net" class="mw-redirect" title="Neural net">Neural net</a> modelling offers a good mathematical model for a comparator as follows: Given a signal S and a threshold "thr", subtract "thr" from S and substitute this difference d to a <a href="Sigmoid_function" title="Sigmoid function">sigmoid function</a>: For large "gains" k, e.g. k=100, 1/( 1 + e<sup>−k*d</sup> ) = 1/( 1 + e<sup>−k*(S-thr)</sup> ) = { ≃0, ≃1 }. For example, if "The door is DOWN" means "The door is less than 50% of the way up", then a threshold thr=0.5 corresponding to 0.5*5.0 = +2.50 volts could be applied to a "linear" measuring-device with an output of 0 volts when fully closed and +5.0 volts when fully open.</span>

</li>

<li id="cite_note-8"><span class="mw-cite-backlink"><b><a href="#cite_ref-8">^</a></b></span> <span class="reference-text">In actuality the digital 1 and 0 are defined over non-overlapping ranges e.g. { "1" = +5/+0.2/−1.0 volts, 0 = +0.5/−0.2 volts }. When a value falls outside the defined range(s) the value becomes "u" -- unknown; e.g. +2.3 would be "u".</span>

</li>

<li id="cite_note-9"><span class="mw-cite-backlink"><b><a href="#cite_ref-9">^</a></b></span> <span class="reference-text">While the notion of logical product is not so peculiar (e.g. 0*0=0, 0*1=0, 1*0=0, 1*1=1), the notion of (1+1=1 <i>is</i> peculiar; in fact (a "+" b) = (a + (b - a*b)) where "+" is the "logical sum" but + and - are the true arithmetic counterparts. Occasionally all four notions do appear in a formula: A AND B = 1/2*( A plus B minus ( A XOR B ) ] (cf p. 146 in John Wakerly 1978, <i>Error Detecting Codes, Self-Checking Circuits and Applications</i>, North-Holland, New York, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-444-00259-6</bdi> pbk.)</span>

</li>

<li id="cite_note-10"><span class="mw-cite-backlink"><b><a href="#cite_ref-10">^</a></b></span> <span class="reference-text">A careful look at its Karnaugh map shows that IF...THEN...ELSE can also be expressed, in a rather round-about way, in terms of two exclusive-ORs: ( (b AND (c XOR a)) OR (a AND (c XOR b)) ) = d.</span>

</li>

<li id="cite_note-11"><span class="mw-cite-backlink"><b><a href="#cite_ref-11">^</a></b></span> <span class="reference-text">Robbin p. 3.</span>

</li>

<li id="cite_note-FOOTNOTERosenbloom195030_and_54ff-12"><span class="mw-cite-backlink"><b><a href="#cite_ref-FOOTNOTERosenbloom195030_and_54ff_12-0">^</a></b></span> <span class="reference-text"><a href="#CITEREFRosenbloom1950">Rosenbloom 1950</a>, pp. 30 and 54ff.</span>

</li>

<li id="cite_note-14"><span class="mw-cite-backlink"><b><a href="#cite_ref-14">^</a></b></span> <span class="reference-text">Indeed, exhaustive selection between alternatives -- <b>mutual exclusion</b> -- is required by the definition that Kleene gives the CASE operator (Kleene 1952229)</span>

</li>

<li id="cite_note-15"><span class="mw-cite-backlink"><b><a href="#cite_ref-15">^</a></b></span> <span class="reference-text">The use of quote marks around the expressions is not accidental. Tarski comments on the use of quotes in his "18. Identity of things and identity of their designations; use of quotation marks" p. 58ff.</span>

</li>

<li id="cite_note-16"><span class="mw-cite-backlink"><b><a href="#cite_ref-16">^</a></b></span> <span class="reference-text">Hamilton p. 37. Bender and Williamson p. 29 state "In what follows, we'll replace "equals" with the symbol " ⇔ " (equivalence) which is usually used in logic. We use the more familiar " = " for assigning meaning and values."</span>

</li>

<li id="cite_note-17"><span class="mw-cite-backlink"><b><a href="#cite_ref-17">^</a></b></span> <span class="reference-text">Reichenbach p. 20-22 and follows the conventions of PM. The symbol =<sub>Df</sub> is in the <a href="Metalanguage" title="Metalanguage">metalanguage</a> and is not a formal symbol with the following meaning: "by symbol ' s ' is to have the same meaning as the formula '(c & d)' ".</span>

</li>

<li id="cite_note-FOOTNOTERosenbloom195032-18"><span class="mw-cite-backlink"><b><a href="#cite_ref-FOOTNOTERosenbloom195032_18-0">^</a></b></span> <span class="reference-text"><a href="#CITEREFRosenbloom1950">Rosenbloom 1950</a>, p. 32.</span>

</li>

<li id="cite_note-20"><span class="mw-cite-backlink"><b><a href="#cite_ref-20">^</a></b></span> <span class="reference-text">cf Minsky 1967:75, section 4.2.3 "The method of parenthesis counting". Minsky presents a state machine that will do the job, and by use of induction (recursive definition) Minsky proves the "method" and presents a theorem as the result. A fully generalized "parenthesis grammar" requires an infinite state machine (e.g. a Turing machine) to do the counting.</span>

</li>

<li id="cite_note-21"><span class="mw-cite-backlink"><b><a href="#cite_ref-21">^</a></b></span> <span class="reference-text">Robbin p. 7</span>

</li>

<li id="cite_note-22"><span class="mw-cite-backlink"><b><a href="#cite_ref-22">^</a></b></span> <span class="reference-text">cf Reichenbach p. 68 for a more involved discussion: "If the inference is valid and the premises are true, the inference is called <i>conclusive</i>.</span>

</li>

<li id="cite_note-23"><span class="mw-cite-backlink"><b><a href="#cite_ref-23">^</a></b></span> <span class="reference-text">As well as the first three, Hamilton pp.19-22 discusses logics built from only | (NAND), and ↓ (NOR).</span>

</li>

<li id="cite_note-24"><span class="mw-cite-backlink"><b><a href="#cite_ref-24">^</a></b></span> <span class="reference-text">Wickes 1967:36ff. Wickes offers a good example of 8 of the 2 x 4 (3-variable maps) and 16 of the 4 x 4 (4-variable) maps. As an arbitrary 3-variable map could represent any one of 2<sup>8</sup>=256 2x4 maps, and an arbitrary 4-variable map could represent any one of 2<sup>16</sup> = 65,536 different formula-evaluations, writing down every one is infeasible.</span>

</li>

<li id="cite_note-25"><span class="mw-cite-backlink"><b><a href="#cite_ref-25">^</a></b></span> <span class="reference-text">This definition is given by <a href="Stephen_Kleene" class="mw-redirect" title="Stephen Kleene">Stephen Kleene</a>. Both <a href="Kurt_G%C3%B6del" title="Kurt Gödel">Kurt Gödel</a> and Kleene believed that the classical paradoxes are uniformly examples of this sort of definition. But Kleene went on to assert that the problem has not been solved satisfactorily and impredicative definitions can be found in <a href="Analysis" title="Analysis">analysis</a>. He gives as example the definition of the <a href="Least_upper_bound" class="mw-redirect" title="Least upper bound">least upper bound</a> (l.u.b) <b>u</b> of <b>M</b>. Given a <a href="Dedekind_cut" title="Dedekind cut">Dedekind cut</a> of the number line <b>C</b> and the two parts into which the number line is cut, i.e. <b>M</b> and (<b>C</b> - <b>M</b>), l.u.b. = <b>u</b> is defined in terms of the notion <b>M</b>, whereas <b>M</b> is defined in terms of <b>C</b>. Thus the definition of <b>u</b>, an element of <b>C</b>, is defined in terms of the totality <b>C</b> and this makes its definition impredicative. Kleene asserts that attempts to argue this away can be used to uphold the impredicative definitions in the paradoxes.(Kleene 1952:43).</span>

</li>

<li id="cite_note-26"><span class="mw-cite-backlink"><b><a href="#cite_ref-26">^</a></b></span> <span class="reference-text">McCluskey comments that "it could be argued that the analysis is still incomplete because the word statement "The outputs are equal to the previous values of the inputs" has not been obtained"; he goes on to dismiss such worries because "English is not a formal language in a mathematical sense, [and] it is not really possible to have a <i>formal</i> procedure for obtaining word statements" (p. 185).</span>

</li>

<li id="cite_note-27"><span class="mw-cite-backlink"><b><a href="#cite_ref-27">^</a></b></span> <span class="reference-text">More precisely, given enough "loop gain", either oscillation or memory will occur (cf McCluskey p. 191-2). In abstract (idealized) mathematical systems adequate loop gain is not a problem.</span>

</li>

<li id="cite_note-28"><span class="mw-cite-backlink"><b><a href="#cite_ref-28">^</a></b></span> <span class="reference-text">The notion of delay and the principle of local causation as caused ultimately by the speed of light appears in Robin Gandy (1980), "Church's thesis and Principles for Mechanisms", in J. Barwise, H. J. Keisler and K. Kunen, eds., <i>The Kleene Symposium</i>, North-Holland Publishing Company (1980) 123-148. Gandy considered this to be the most important of his principles: "Contemporary physics rejects the possibility of instantaneous action at a distance" (p. 135). Gandy was <a href="Alan_Turing" title="Alan Turing">Alan Turing</a>'s student and close friend.</span>

</li>

<li id="cite_note-29"><span class="mw-cite-backlink"><b><a href="#cite_ref-29">^</a></b></span> <span class="reference-text">McKlusky p. 194-5 discusses "breaking the loop" and inserts "amplifiers" to do this; Wickes (p. 118-121) discuss inserting delays. McCluskey p. 195ff discusses the problem of "races" caused by delays.</span>

</li>

</ol></div></div>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

<ul><li><cite id="CITEREFRosenbloom1950" class="citation book cs1"><a href="Paul_C._Rosenbloom" title="Paul C. Rosenbloom">Rosenbloom, Paul</a> (1950). <i>The Elements of Mathematical Logic</i>. Mineola, New York: Dover Publications, Inc. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-486-44617-4</bdi>.</cite> <span class="cs1-hidden-error citation-comment"><code class="cs1-code">{{cite book}}</code>: </span><span class="cs1-hidden-error citation-comment">ISBN / Date incompatibility (help)</span></li>

<li><cite id="CITEREFKleene1952" class="citation book cs1"><a href="Stephen_Cole_Kleene" title="Stephen Cole Kleene">Kleene, Stephen</a> (1952). <i>Introduction to metamathematics</i>. Amsterdam: North-Holland Publishing Company.</cite></li>

/* start https://en.wikipedia.org/ */

.mw-parser-output span.smallcaps{font-variant:small-caps}.mw-parser-output span.smallcaps-smaller{font-size:85%}

/* end https://en.wikipedia.org/ */

</style><span class="smallcaps">Bender, Edward A.</span> and <span class="smallcaps">Williamson, S. Gill</span>, 2005, <i>A Short Course in Discrete Mathematics</i>, Dover Publications, Mineola NY, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-486-43946-1</bdi>. This text is used in a "lower division two-quarter [computer science] course" at UC San Diego.</li>

<li><span class="smallcaps"><a href="Herbert_Enderton" title="Herbert Enderton">Enderton, H. B.</a></span>, 2002, <i>A Mathematical Introduction to Logic.</i> Harcourt/Academic Press. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-12-238452-0</bdi></li>

<li><span class="smallcaps">Goodstein, R. L.</span>, (Pergamon Press 1963), 1966, (Dover edition 2007), <i>Boolean Algebra</i>, Dover Publications, Inc. Minola, New York, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-486-45894-6</bdi>. Emphasis on the notion of "algebra of classes" with set-theoretic symbols such as ∩, ∪, ' (NOT), ⊂ (IMPLIES). Later Goldstein replaces these with &, ∨, ￢, → (respectively) in his treatment of "Sentence Logic" pp. 76–93.</li>

<li><span class="smallcaps"><a href="Ivor_Grattan-Guinness" title="Ivor Grattan-Guinness">Ivor Grattan-Guinness</a></span> and Gérard Bornet 1997, <i>George Boole: Selected Manuscripts on Logic and its Philosophy</i>, Birkhäuser Verlag, Basil, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-8176-5456-6</bdi> (Boston).</li>

<li><span class="smallcaps">A. G. Hamilton</span> 1978, <i>Logic for Mathematicians</i>, Cambridge University Press, Cambridge UK, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-521-21838-1</bdi>.</li>

<li><span class="smallcaps">E. J. <a href="McCluskey" title="McCluskey">McCluskey</a></span> 1965, <i>Introduction to the Theory of Switching Circuits</i>, McGraw-Hill Book Company, New York. No ISBN. Library of Congress Catalog Card Number 65-17394. McCluskey was a student of <a href="Willard_Quine" class="mw-redirect" title="Willard Quine">Willard Quine</a> and developed some notable theorems with Quine and on his own. For those interested in the history, the book contains a wealth of references.</li>

<li><span class="smallcaps"><a href="Marvin_L._Minsky" class="mw-redirect" title="Marvin L. Minsky">Marvin L. Minsky</a></span> 1967, <i>Computation: Finite and Infinite Machines</i>, Prentice-Hall, Inc, Englewood Cliffs, N.J.. No ISBN. Library of Congress Catalog Card Number 67-12342. Useful especially for computability, plus good sources.</li>

<li><span class="smallcaps">Joel W. Robbin</span> 1969, 1997, <i>Mathematical Logic: A First Course</i>, Dover Publications, Inc., Mineola, New York, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-486-45018-X</bdi> (pbk.).</li>

<li><span class="smallcaps"><a href="Patrick_Suppes" title="Patrick Suppes">Patrick Suppes</a></span> 1957 (1999 Dover edition), <i>Introduction to Logic</i>, Dover Publications, Inc., Mineola, New York. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-486-40687-3</bdi> (pbk.). This book is in print and readily available.</li>

<li>On his page 204 in a footnote he references his set of axioms to <a href="Edward_Vermilye_Huntington" title="Edward Vermilye Huntington">E. V. Huntington</a>, "Sets of Independent Postulates for the Algebra of Logic", <i>Transactions of the American Mathematical Society</i>, Vol. 5 91904) pp. 288-309.</li>

<li><span class="smallcaps"><a href="Alfred_Tarski" title="Alfred Tarski">Alfred Tarski</a></span> 1941 (1995 Dover edition), <i>Introduction to Logic and to the Methodology of Deductive Sciences</i>, Dover Publications, Inc., Mineola, New York. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-486-28462-X</bdi> (pbk.). This book is in print and readily available.</li>

<li><span class="smallcaps"><a href="Jean_van_Heijenoort" title="Jean van Heijenoort">Jean van Heijenoort</a></span> 1967, 3rd printing with emendations 1976, <i>From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931</i>, Harvard University Press, Cambridge, Massachusetts. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-674-32449-8</bdi> (pbk.) Translation/reprints of Frege (1879), Russell's letter to Frege (1902) and Frege's letter to Russell (1902), Richard's paradox (1905), Post (1921) can be found here.</li>

<li><span class="smallcaps"><a href="Alfred_North_Whitehead" title="Alfred North Whitehead">Alfred North Whitehead</a></span> and <span class="smallcaps"><a href="Bertrand_Russell" title="Bertrand Russell">Bertrand Russell</a></span> 1927 2nd edition, paperback edition to *53 1962, <i>Principia Mathematica</i>, Cambridge University Press, no ISBN. In the years between the first edition of 1912 and the 2nd edition of 1927, H. M. <a href="Sheffer" title="Sheffer">Sheffer</a> 1921 and M. Jean <a href="Nicod" class="mw-redirect" title="Nicod">Nicod</a> (no year cited) brought to Russell's and Whitehead's attention that what they considered their primitive propositions (connectives) could be reduced to a single |, nowadays known as the "stroke" or NAND (NOT-AND, NEITHER ... NOR...). Russell-Whitehead discuss this in their "Introduction to the Second Edition" and makes the definitions as discussed above.</li>

<li><span class="smallcaps">William E. Wickes</span> 1968, <i>Logic Design with Integrated Circuits</i>, John Wiley & Sons, Inc., New York. No ISBN. Library of Congress Catalog Card Number: 68-21185. Tight presentation of engineering's analysis and synthesis methods, references McCluskey 1965. Unlike Suppes, Wickes' presentation of "Boolean algebra" starts with a set of postulates of a truth-table nature and then derives the customary theorems of them (p. 18ff).</li></ul>

<div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2></div>

<ul><li><span class="noviewer" typeof="mw:File"></span> Media related to <a href="https://commons.wikimedia.org/wiki/Category:Propositional_formula" class="extiw external" title="commons:Category:Propositional formula">Propositional formula</a> at Wikimedia Commons</li></ul>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}

/* end https://en.wikipedia.org/ */

</style><style data-mw-deduplicate="TemplateStyles:r1236075235">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style></div><div role="navigation" class="navbox" aria-labelledby="Mathematical_logic344" style="padding:3px"><table class="nowraplinks mw-collapsible mw-collapsed navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><style data-mw-deduplicate="TemplateStyles:r1239400231">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbar{display:inline;font-size:88%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar a>span,.mw-parser-output .navbar a>abbr{text-decoration:inherit}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}html.skin-theme-clientpref-night .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}}@media print{.mw-parser-output .navbar{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div id="Mathematical_logic344" style="font-size:114%;margin:0 4em"><a href="Mathematical_logic" title="Mathematical logic">Mathematical logic</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">General</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Axiom" title="Axiom">Axiom</a>

<li><a href="Cardinality" title="Cardinality">Cardinality</a></li>

<li><a href="First-order_logic" title="First-order logic">First-order logic</a></li>

<li><a href="Formal_proof" title="Formal proof">Formal proof</a></li>

<li><a href="Formal_semantics_(logic)" class="mw-redirect" title="Formal semantics (logic)">Formal semantics</a></li>

<li><a href="Foundations_of_mathematics" title="Foundations of mathematics">Foundations of mathematics</a></li>

<li><a href="Information_theory" title="Information theory">Information theory</a></li>

<li><a href="Lemma_(mathematics)" title="Lemma (mathematics)">Lemma</a></li>

<li><a href="Logical_consequence" title="Logical consequence">Logical consequence</a></li>

<li><a href="Structure_(mathematical_logic)" title="Structure (mathematical logic)">Model</a></li>

<li><a href="Theorem" title="Theorem">Theorem</a></li>

<li><a href="Theory_(mathematical_logic)" title="Theory (mathematical logic)">Theory</a></li>

<li><a href="Type_theory" title="Type theory">Type theory</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Theorems (list)<br> and <a href="Paradoxes_of_set_theory" title="Paradoxes of set theory">paradoxes</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="G%C3%B6del's_completeness_theorem" title="Gödel's completeness theorem">Gödel's completeness</a> and <a href="G%C3%B6del's_incompleteness_theorems" title="Gödel's incompleteness theorems">incompleteness theorems</a></li>

<li><a href="Tarski's_undefinability_theorem" title="Tarski's undefinability theorem">Tarski's undefinability</a></li>

<li><a href="Banach%E2%80%93Tarski_paradox" title="Banach–Tarski paradox">Banach–Tarski paradox</a></li>

<li>Cantor's <a href="Cantor's_theorem" title="Cantor's theorem">theorem,</a> <a href="Cantor's_paradox" title="Cantor's paradox">paradox</a> and <a href="Cantor's_diagonal_argument" title="Cantor's diagonal argument">diagonal argument</a></li>

<li><a href="Compactness_theorem" title="Compactness theorem">Compactness</a></li>

<li><a href="Halting_problem" title="Halting problem">Halting problem</a></li>

<li><a href="Lindstr%C3%B6m's_theorem" title="Lindström's theorem">Lindström's</a></li>

<li><a href="L%C3%B6wenheim%E2%80%93Skolem_theorem" title="Löwenheim–Skolem theorem">Löwenheim–Skolem</a></li>

<li><a href="Russell's_paradox" title="Russell's paradox">Russell's paradox</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Logic" title="Logic">Logics</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th id="Traditional95" scope="row" class="navbox-group" style="width:1%"><a href="Term_logic" title="Term logic">Traditional</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Classical_logic" title="Classical logic">Classical logic</a></li>

<li><a href="Logical_truth" title="Logical truth">Logical truth</a></li>

<li><a href="Tautology_(logic)" title="Tautology (logic)">Tautology</a></li>

<li><a href="Proposition" title="Proposition">Proposition</a></li>

<li><a href="Inference" title="Inference">Inference</a></li>

<li><a href="Logical_equivalence" title="Logical equivalence">Logical equivalence</a></li>

<li><a href="Consistency" title="Consistency">Consistency</a>

<ul><li><a href="Equiconsistency" title="Equiconsistency">Equiconsistency</a></li></ul></li>

<li><a href="Argument" title="Argument">Argument</a></li>

<li><a href="Soundness" title="Soundness">Soundness</a></li>

<li><a href="Validity_(logic)" title="Validity (logic)">Validity</a></li>

<li><a href="Syllogism" title="Syllogism">Syllogism</a></li>

<li><a href="Square_of_opposition" title="Square of opposition">Square of opposition</a></li>

<li><a href="Venn_diagram" title="Venn diagram">Venn diagram</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Propositional_calculus" class="mw-redirect" title="Propositional calculus">Propositional</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Boolean_algebra" title="Boolean algebra">Boolean algebra</a></li>

<li><a href="Boolean_function" title="Boolean function">Boolean functions</a></li>

<li><a href="Logical_connective" title="Logical connective">Logical connectives</a></li>

<li><a href="Propositional_calculus" class="mw-redirect" title="Propositional calculus">Propositional calculus</a></li>

<li><a href="Truth_table" title="Truth table">Truth tables</a></li>

<li><a href="Many-valued_logic" title="Many-valued logic">Many-valued logic</a>

<li><a href="Finite-valued_logic" title="Finite-valued logic">finite</a></li>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Predicate_logic" class="mw-redirect" title="Predicate logic">Predicate</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="First-order_logic" title="First-order logic">First-order</a>

<li><a href="Second-order_logic" title="Second-order logic">Second-order</a>

<ul><li><a href="Monadic_second-order_logic" title="Monadic second-order logic">Monadic</a></li></ul></li>

<li><a href="Higher-order_logic" title="Higher-order logic">Higher-order</a></li>

<li><a href="Fixed-point_logic" title="Fixed-point logic">Fixed-point</a></li>

<li><a href="Quantifier_(logic)" title="Quantifier (logic)">Quantifiers</a></li>

<li><a href="Predicate_(mathematical_logic)" class="mw-redirect" title="Predicate (mathematical logic)">Predicate</a></li>

<li><a href="Monadic_predicate_calculus" title="Monadic predicate calculus">Monadic predicate calculus</a></li></ul>

</div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Set_theory" title="Set theory">Set theory</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><td colspan="2" class="navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Hereditary_set" title="Hereditary set">hereditary</a></li></ul></li>

<li><a href="Class_(set_theory)" title="Class (set theory)">Class</a></li>

<li>(<a href="Urelement" title="Urelement">Ur-</a>)<a href="Element_(mathematics)" title="Element (mathematics)">Element</a></li>

<li><a href="Ordinal_number" title="Ordinal number">Ordinal number</a></li>

<li><a href="Extensionality" title="Extensionality">Extensionality</a></li>

<li><a href="Forcing_(mathematics)" title="Forcing (mathematics)">Forcing</a></li>

<li><a href="Relation_(mathematics)" title="Relation (mathematics)">Relation</a>

<ul><li><a href="Equivalence_relation" title="Equivalence relation">equivalence</a></li>

<li><a href="Partition_of_a_set" title="Partition of a set">partition</a></li></ul></li>

<li>Set operations:

<ul><li><a href="Intersection_(set_theory)" title="Intersection (set theory)">intersection</a></li>

<li><a href="Union_(set_theory)" title="Union (set theory)">union</a></li>

<li><a href="Complement_(set_theory)" title="Complement (set theory)">complement</a></li>

<li><a href="Cartesian_product" title="Cartesian product">Cartesian product</a></li>

<li><a href="Power_set" title="Power set">power set</a></li>

<li><a href="List_of_set_identities_and_relations" title="List of set identities and relations">identities</a></li></ul></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Types of <a href="Set_(mathematics)" title="Set (mathematics)">sets</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Countable_set" title="Countable set">Countable</a></li>

<li><a href="Uncountable_set" title="Uncountable set">Uncountable</a></li>

<li><a href="Empty_set" title="Empty set">Empty</a></li>

<li><a href="Inhabited_set" title="Inhabited set">Inhabited</a></li>

<li><a href="Singleton_(mathematics)" title="Singleton (mathematics)">Singleton</a></li>

<li><a href="Finite_set" title="Finite set">Finite</a></li>

<li><a href="Infinite_set" title="Infinite set">Infinite</a></li>

<li><a href="Transitive_set" title="Transitive set">Transitive</a></li>

<li><a href="Ultrafilter_(set_theory)" class="mw-redirect" title="Ultrafilter (set theory)">Ultrafilter</a></li>

<li><a href="Recursive_set" class="mw-redirect" title="Recursive set">Recursive</a></li>

<li><a href="Fuzzy_set" title="Fuzzy set">Fuzzy</a></li>

<li><a href="Universal_set" title="Universal set">Universal</a></li>

<li><a href="Universe_(mathematics)" title="Universe (mathematics)">Universe</a>

<ul><li><a href="Constructible_universe" title="Constructible universe">constructible</a></li>

<li><a href="Grothendieck_universe" title="Grothendieck universe">Grothendieck</a></li>

<li><a href="Von_Neumann_universe" title="Von Neumann universe">Von Neumann</a></li></ul></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Map_(mathematics)" title="Map (mathematics)">Maps</a> and <a href="Cardinality" title="Cardinality">cardinality</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Function_(mathematics)" title="Function (mathematics)">Function</a>/<a href="Map_(mathematics)" title="Map (mathematics)">Map</a>

<ul><li><a href="Domain_of_a_function" title="Domain of a function">domain</a></li>

<li><a href="Codomain" title="Codomain">codomain</a></li>

<li><a href="Image_(mathematics)" title="Image (mathematics)">image</a></li></ul></li>

<li><a href="Injective_function" title="Injective function">In</a>/<a href="Surjective_function" title="Surjective function">Sur</a>/<a href="Bijection" title="Bijection">Bi</a>-jection</li>

<li><a href="Schr%C3%B6der%E2%80%93Bernstein_theorem" title="Schröder–Bernstein theorem">Schröder–Bernstein theorem</a></li>

<li><a href="Isomorphism" title="Isomorphism">Isomorphism</a></li>

<li><a href="G%C3%B6del_numbering" title="Gödel numbering">Gödel numbering</a></li>

<li><a href="Enumeration" title="Enumeration">Enumeration</a></li>

<li><a href="Large_cardinal" title="Large cardinal">Large cardinal</a>

<ul><li><a href="Inaccessible_cardinal" title="Inaccessible cardinal">inaccessible</a></li></ul></li>

<li><a href="Aleph_number" title="Aleph number">Aleph number</a></li>

<li><a href="Operation_(mathematics)" title="Operation (mathematics)">Operation</a>

<ul><li><a href="Binary_operation" title="Binary operation">binary</a></li></ul></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Set theories</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Zermelo%E2%80%93Fraenkel_set_theory" title="Zermelo–Fraenkel set theory">Zermelo–Fraenkel</a>

<ul><li><a href="Axiom_of_choice" title="Axiom of choice">axiom of choice</a></li>

<li><a href="Continuum_hypothesis" title="Continuum hypothesis">continuum hypothesis</a></li></ul></li>

<li><a href="General_set_theory" title="General set theory">General</a></li>

<li><a href="Kripke%E2%80%93Platek_set_theory" title="Kripke–Platek set theory">Kripke–Platek</a></li>

<li><a href="Morse%E2%80%93Kelley_set_theory" title="Morse–Kelley set theory">Morse–Kelley</a></li>

<li><a href="Naive_set_theory" title="Naive set theory">Naive</a></li>

<li><a href="New_Foundations" title="New Foundations">New Foundations</a></li>

<li><a href="Tarski%E2%80%93Grothendieck_set_theory" title="Tarski–Grothendieck set theory">Tarski–Grothendieck</a></li>

<li><a href="Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory" title="Von Neumann–Bernays–Gödel set theory">Von Neumann–Bernays–Gödel</a></li>

<li><a href="Ackermann_set_theory" title="Ackermann set theory">Ackermann</a></li>

<li><a href="Constructive_set_theory" title="Constructive set theory">Constructive</a></li></ul>

</div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Formal_system" title="Formal system">Formal systems</a> (<a href="List_of_formal_systems" title="List of formal systems"><span style="font-size: 85%;">list</span></a>),<br><a href="Formal_language" title="Formal language">language</a> and <a href="Syntax_(logic)" title="Syntax (logic)">syntax</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><td colspan="2" class="navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Alphabet_(formal_languages)" title="Alphabet (formal languages)">Alphabet</a></li>

<li><a href="Arity" title="Arity">Arity</a></li>

<li><a href="Automata_theory" title="Automata theory">Automata</a></li>

<li><a href="Axiom_schema" title="Axiom schema">Axiom schema</a></li>

<li><a href="Expression_(mathematics)" title="Expression (mathematics)">Expression</a>

<ul><li><a href="Ground_expression" title="Ground expression">ground</a></li></ul></li>

<li><a href="Extension_by_new_constant_and_function_names" title="Extension by new constant and function names">Extension</a>

<ul><li><a href="Extension_by_definitions" class="mw-redirect" title="Extension by definitions">by definition</a></li>

<li><a href="Conservative_extension" title="Conservative extension">conservative</a></li></ul></li>

<li><a href="Finitary_relation" title="Finitary relation">Relation</a></li>

<li><a href="Formation_rule" title="Formation rule">Formation rule</a></li>

<li><a href="Formal_grammar" title="Formal grammar">Grammar</a></li>

<li><a href="Well-formed_formula" title="Well-formed formula">Formula</a>

<ul><li><a href="Atomic_formula" title="Atomic formula">atomic</a></li>

<li><a href="Sentence_(mathematical_logic)" title="Sentence (mathematical logic)">closed</a></li>

<li><a href="Ground_formula" class="mw-redirect" title="Ground formula">ground</a></li>

<li><a href="Free_variables_and_bound_variables" title="Free variables and bound variables">Free/bound variable</a></li>

<li><a href="Formal_language" title="Formal language">Language</a></li>

<li><a href="Metalanguage" title="Metalanguage">Metalanguage</a></li>

<li><a href="Logical_connective" title="Logical connective">Logical connective</a>

<li><a href="Predicate_(mathematical_logic)" class="mw-redirect" title="Predicate (mathematical logic)">Predicate</a>

<ul><li><a href="Functional_predicate" title="Functional predicate">functional</a></li>

<li><a href="Predicate_variable" title="Predicate variable">variable</a></li>

<li><a href="Propositional_variable" title="Propositional variable">propositional variable</a></li></ul></li>

<li><a href="Formal_proof" title="Formal proof">Proof</a></li>

<li><a href="Quantifier_(logic)" title="Quantifier (logic)">Quantifier</a>

<li><a href="Sentence_(mathematical_logic)" title="Sentence (mathematical logic)">Sentence</a>

<ul><li><a href="Atomic_sentence" title="Atomic sentence">atomic</a></li>

<li><a href="Spectrum_of_a_sentence" title="Spectrum of a sentence">spectrum</a></li></ul></li>

<li><a href="Signature_(logic)" title="Signature (logic)">Signature</a></li>

<li><a href="String_(formal_languages)" class="mw-redirect" title="String (formal languages)">String</a></li>

<li><a href="Substitution_(logic)" title="Substitution (logic)">Substitution</a></li>

<li><a href="Symbol_(formal)" title="Symbol (formal)">Symbol</a>

<ul><li><a href="Uninterpreted_function" title="Uninterpreted function">function</a></li>

<li><a href="Logical_constant" title="Logical constant">logical/constant</a></li>

<li><a href="Non-logical_symbol" title="Non-logical symbol">non-logical</a></li>

<li><a href="Variable_(mathematics)" title="Variable (mathematics)">variable</a></li></ul></li>

<li><a href="Theory_(mathematical_logic)" title="Theory (mathematical logic)">Theory</a>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><span class="nowrap">Example <a href="Axiomatic_system" title="Axiomatic system">axiomatic<br>systems</a> <span style="font-size: 85%;">(<a href="List_of_first-order_theories" title="List of first-order theories">list</a>)</span></span></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li>of <a href="True_arithmetic" title="True arithmetic">arithmetic</a>:

<ul><li><a href="Peano_axioms" title="Peano axioms">Peano</a></li>

<li><a href="Second-order_arithmetic" title="Second-order arithmetic">second-order</a></li>

<li><a href="Elementary_function_arithmetic" title="Elementary function arithmetic">elementary function</a></li>

<li><a href="Primitive_recursive_arithmetic" title="Primitive recursive arithmetic">primitive recursive</a></li>

<li><a href="Robinson_arithmetic" title="Robinson arithmetic">Robinson</a></li>

<li><a href="Skolem_arithmetic" title="Skolem arithmetic">Skolem</a></li></ul></li>

<li>of the <a href="Construction_of_the_real_numbers" title="Construction of the real numbers">real numbers</a>

<ul><li><a href="Tarski's_axiomatization_of_the_reals" title="Tarski's axiomatization of the reals">Tarski's axiomatization</a></li></ul></li>

<li>of <a href="Axiomatization_of_Boolean_algebras" class="mw-redirect" title="Axiomatization of Boolean algebras">Boolean algebras</a>

<ul><li><a href="Boolean_algebras_canonically_defined" title="Boolean algebras canonically defined">canonical</a></li>

<li><a href="Minimal_axioms_for_Boolean_algebra" title="Minimal axioms for Boolean algebra">minimal axioms</a></li></ul></li>

<li>of <a href="Foundations_of_geometry" title="Foundations of geometry">geometry</a>:

<ul><li><a href="Euclidean_geometry" title="Euclidean geometry">Euclidean</a>:

<ul><li><a href="Euclid's_Elements" title="Euclid's Elements"><i>Elements</i></a></li>

<li><a href="Hilbert's_axioms" title="Hilbert's axioms">Hilbert's</a></li>

<li><a href="Tarski's_axioms" title="Tarski's axioms">Tarski's</a></li></ul></li>

<li><a href="Non-Euclidean_geometry" title="Non-Euclidean geometry">non-Euclidean</a></li></ul></li></ul>

<ul><li><i><a href="Principia_Mathematica" title="Principia Mathematica">Principia Mathematica</a></i></li></ul>

</div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Proof_theory" title="Proof theory">Proof theory</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Formal_proof" title="Formal proof">Formal proof</a></li>

<li><a href="Natural_deduction" title="Natural deduction">Natural deduction</a></li>

<li><a href="Logical_consequence" title="Logical consequence">Logical consequence</a></li>

<li><a href="Rule_of_inference" title="Rule of inference">Rule of inference</a></li>

<li><a href="Sequent_calculus" title="Sequent calculus">Sequent calculus</a></li>

<li><a href="Theorem" title="Theorem">Theorem</a></li>

<li><a href="Formal_system" title="Formal system">Systems</a>

<ul><li><a href="Axiomatic_system" title="Axiomatic system">axiomatic</a></li>

<li><a href="Deductive_system" class="mw-redirect" title="Deductive system">deductive</a></li>

<li><a href="Hilbert_system" title="Hilbert system">Hilbert</a>

<li><a href="Complete_theory" title="Complete theory">Complete theory</a></li>

<li><a href="Independence_(mathematical_logic)" title="Independence (mathematical logic)">Independence</a> (<a href="List_of_statements_independent_of_ZFC" title="List of statements independent of ZFC">from ZFC</a>)</li>

<li><a href="Proof_of_impossibility" title="Proof of impossibility">Proof of impossibility</a></li>

<li><a href="Ordinal_analysis" title="Ordinal analysis">Ordinal analysis</a></li>

<li><a href="Reverse_mathematics" title="Reverse mathematics">Reverse mathematics</a></li>

<li><a href="Self-verifying_theories" title="Self-verifying theories">Self-verifying theories</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Model_theory" title="Model theory">Model theory</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Interpretation_(logic)" title="Interpretation (logic)">Interpretation</a>

<ul><li><a href="Interpretation_function" class="mw-redirect" title="Interpretation function">function</a></li>

<li><a href="Interpretation_(model_theory)" title="Interpretation (model theory)">of models</a></li></ul></li>

<li><a href="Structure_(mathematical_logic)" title="Structure (mathematical logic)">Model</a>

<ul><li><a href="Elementary_equivalence" title="Elementary equivalence">equivalence</a></li>

<li><a href="Finite_model_theory" title="Finite model theory">finite</a></li>

<li><a href="Saturated_model" title="Saturated model">saturated</a></li>

<li><a href="Spectrum_of_a_theory" title="Spectrum of a theory">spectrum</a></li>

<li><a href="Substructure_(mathematics)" title="Substructure (mathematics)">submodel</a></li></ul></li>

<li><a href="Non-standard_model" title="Non-standard model">Non-standard model</a>

<ul><li><a href="Non-standard_model_of_arithmetic" title="Non-standard model of arithmetic">of arithmetic</a></li></ul></li>

<li><a href="Diagram_(mathematical_logic)" title="Diagram (mathematical logic)">Diagram</a>

<ul><li><a href="Elementary_diagram" title="Elementary diagram">elementary</a></li></ul></li>

<li><a href="Categorical_theory" title="Categorical theory">Categorical theory</a></li>

<li><a href="Model_complete_theory" title="Model complete theory">Model complete theory</a></li>

<li><a href="Satisfiability" title="Satisfiability">Satisfiability</a></li>

<li><a href="Semantics_of_logic" title="Semantics of logic">Semantics of logic</a></li>

<li><a href="Strength_(mathematical_logic)" title="Strength (mathematical logic)">Strength</a></li>

<li><a href="Theories_of_truth" class="mw-redirect" title="Theories of truth">Theories of truth</a>

<ul><li><a href="Semantic_theory_of_truth" title="Semantic theory of truth">semantic</a></li>

<li><a href="Tarski's_theory_of_truth" class="mw-redirect" title="Tarski's theory of truth">Tarski's</a></li>

<li><a href="Kripke's_theory_of_truth" class="mw-redirect" title="Kripke's theory of truth">Kripke's</a></li></ul></li>

<li><a href="T-schema" title="T-schema">T-schema</a></li>

<li><a href="Transfer_principle" title="Transfer principle">Transfer principle</a></li>

<li><a href="Truth_predicate" title="Truth predicate">Truth predicate</a></li>

<li><a href="Truth_value" title="Truth value">Truth value</a></li>

<li><a href="Ultraproduct" title="Ultraproduct">Ultraproduct</a></li>

<li><a href="Validity_(logic)" title="Validity (logic)">Validity</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Computability_theory" title="Computability theory">Computability theory</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Church_encoding" title="Church encoding">Church encoding</a></li>

<li><a href="Church%E2%80%93Turing_thesis" title="Church–Turing thesis">Church–Turing thesis</a></li>

<li><a href="Computably_enumerable_set" title="Computably enumerable set">Computably enumerable</a></li>

<li><a href="Computable_function" title="Computable function">Computable function</a></li>

<li><a href="Computable_set" title="Computable set">Computable set</a></li>

<li><a href="Decision_problem" title="Decision problem">Decision problem</a>

<ul><li><a href="Decidability_(logic)" title="Decidability (logic)">decidable</a></li>

<li><a href="Undecidable_problem" title="Undecidable problem">undecidable</a></li>

<li><a href="P_versus_NP_problem" title="P versus NP problem">P versus NP problem</a></li></ul></li>

<li><a href="Kolmogorov_complexity" title="Kolmogorov complexity">Kolmogorov complexity</a></li>

<li><a href="Lambda_calculus" title="Lambda calculus">Lambda calculus</a></li>

<li><a href="Primitive_recursive_function" title="Primitive recursive function">Primitive recursive function</a></li>

<li><a href="Recursion" title="Recursion">Recursion</a></li>

<li><a href="Recursive_set" class="mw-redirect" title="Recursive set">Recursive set</a></li>

<li><a href="Turing_machine" title="Turing machine">Turing machine</a></li>

<li><a href="Type_theory" title="Type theory">Type theory</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Related</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Abstract_logic" title="Abstract logic">Abstract logic</a></li>

<li><a href="Algebraic_logic" title="Algebraic logic">Algebraic logic</a></li>

<li><a href="Automated_theorem_proving" title="Automated theorem proving">Automated theorem proving</a></li>

<li><a href="Category_theory" title="Category theory">Category theory</a></li>

<li><a href="Concrete_category" title="Concrete category">Concrete</a>/<a href="Category_(mathematics)" title="Category (mathematics)">Abstract category</a></li>

<li><a href="Category_of_sets" title="Category of sets">Category of sets</a></li>

<li><a href="History_of_logic" title="History of logic">History of logic</a></li>

<li><a href="History_of_mathematical_logic" class="mw-redirect" title="History of mathematical logic">History of mathematical logic</a>

<ul><li><a href="Timeline_of_mathematical_logic" title="Timeline of mathematical logic">timeline</a></li></ul></li>

<li><a href="Logicism" title="Logicism">Logicism</a></li>

<li><a href="Mathematical_object" title="Mathematical object">Mathematical object</a></li>

<li><a href="Philosophy_of_mathematics" title="Philosophy of mathematics">Philosophy of mathematics</a></li>

<li><a href="Supertask" title="Supertask">Supertask</a></li></ul>

</div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div><b><span class="nowrap"><span class="skin-invert-image noviewer" typeof="mw:File"></span> </span><a href="Portal%3AMathematics" title="Portal:Mathematics">Mathematics portal</a></b></div></td></tr></tbody></table></div></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2025-03-24" href="https://en.wikipedia.org/wiki/?title=Propositional_formula&oldid=1282047542">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>